Theorem bitr 173

Description: An inference from transitive law for logical equivalence.

Hypotheses

Ref	Expression
bitr.1	|- (ph <-> ps)
bitr.2	|- (ps <-> ch)

Assertion

Ref	Expression
bitr	|- (ph <-> ch)

Proof of Theorem bitr

Step	Hyp	Ref	Expression
1		bitr.1	. . . 4 |- (ph <-> ps)
2	1	biimp 151	. . 3 |- (ph -> ps)
3		bitr.2	. . . 4 |- (ps <-> ch)
4	3	biimp 151	. . 3 |- (ps -> ch)
5	2, 4	syl 10	. 2 |- (ph -> ch)
6	3	biimpr 152	. . 3 |- (ch -> ps)
7	1	biimpr 152	. . 3 |- (ps -> ph)
8	6, 7	syl 10	. 2 |- (ch -> ph)
9	5, 8	impbi 157	1 |- (ph <-> ch)

Syntax hints:   <-> wb 146

This theorem is referenced by:  bitr2 174  bitr3 175  bitr4 176  3bitr 177  3bitr2 179  3bitr3 181  3bitr4 183  imbi12i 188  dfor2 229  iman 237  orbi12i 257  or42 265  anor 304  oran 312  impexp 347  pm4.14 352  pm4.78 354  anass 441  anbi12i 484  pm5.53 485  an42 509  pm4.11 524  ibibr 593  orddi 608  anddi 609  bibi12i 612  pm4.71r 638  pm5.18 662  nbbn 663  pm5.17 670  dfbi3 672  xor2 675  pm5.55 677  tbt 722  nbn 724  biorfi 738  orbidi 745  biluk 747  ccase 757  ccased 758  prlem2 773  rnlem 775  3orass 780  3anass 781  3ancomb 785  alex 1036  alinexa 1044  exanali 1045  alexn 1046  19.21-2 1059  19.26-2 1070  19.27 1071  19.28 1072  19.36 1080  19.37 1082  19.30 1087  19.44 1091  19.45 1092  alrot4 1099  exrot3 1101  exrot4 1102  albi 1109  2albi 1110  aaan 1121  eeor 1122  sbor 1237  sb19.21 1238  sban 1239  sbbi 1241  sblbis 1242  sbrbis 1243  sbrbif 1244  sbid2 1255  sbco2d 1258  sb8e 1264  19.23vv 1296  19.41vv 1308  19.41vvv 1309  19.42vv 1312  3exdistr 1314  4exdistr 1315  cbvex4v 1324  eeanv 1325  eeeanv 1326  sbcom2 1336  2sb5 1337  2sb6 1338  sb6a 1339  2sb5rf 1340  2sb6rf 1341  sb7f 1343  sbex 1350  sbalv 1351  exsb 1352  2exsb 1353  a12lem2 1379  euf 1386  sb8eu 1392  cbveu 1393  mo 1395  eu2 1398  mo2 1402  mo3 1403  mo4f 1404  eu4 1412  moanim 1429  euan 1430  mopick2 1439  2exeu 1449  2mo 1450  2mos 1451  2eu1 1452  2eu3 1454  2eu4 1455  2eu6 1457  exists1 1460  abid 1468  eqeq12i 1491  eleq12i 1542  abeq2 1571  abeq2i 1573  eq2ab 1576  clabel 1585  sbabel 1587  necon3abii 1599  necon1abii 1619  neanior 1642  ralinexa 1686  rexanali 1687  r3al 1693  r19.26 1753  r19.26-2 1754  r19.43 1768  ralcom 1777  rexcom 1778  ralcom2 1779  reeanv 1781  cbvral2v 1806  cbvral3v 1807  rabeq2i 1813  ceqsex2 1839  vtocl2 1846  vtocl3 1847  vtoclgf 1849  cla4gf 1863  cla43gv 1870  eqvincf 1887  ceqsrex2v 1893  elrab2 1910  euxfr2 1929  euxfr 1930  reu2 1933  rmo4 1936  reu4 1937  reu7 1938  2reuswap 1940  sbralie 1944  sbccomglem 1992  ra5 2004  dfss 2058  ss2ab 2120  dfpss2 2137  psseq12i 2143  pssn2lp 2151  sspsstri 2152  uneqri 2178  ssequn2 2207  unss 2208  ineqri 2213  sseqin2 2233  nssinpss 2244  nsspssun 2245  dfss4 2246  difin 2249  symdif2 2270  inrab2 2276  reuun2 2282  rab0 2298  eq0 2299  0el 2301  0pss 2313  npss0 2314  disj1 2317  disjpss 2324  undif4 2330  difin0ss 2337  inssdif0 2338  r19.3rzv 2353  ralidm 2362  dfpr2 2427  ralpr 2433  rexpr 2434  eusn 2451  eldifsn 2467  difprsn 2470  pw0 2473  pwpw0 2474  eqsn 2479  prsspw 2485  prel12 2489  preqsn 2491  pwsnALT 2506  eluniab 2518  elunirab 2519  unipr 2520  uniun 2524  uniin 2525  unissb 2533  elintab 2549  elintrab 2550  ssintab 2555  intun 2567  intpr 2568  iuniin 2578  iuneq2 2583  dfiun2g 2591  dfiin2 2593  iunss 2596  iunid 2608  iun0 2609  0iun 2610  iunxsn 2618  iunun 2619  iunxun 2620  iununi 2622  iunpwss 2624  inex1 2722  pwex 2752  pwssb 2767  exss 2776  dtru 2779  zfpair2 2787  elop 2790  copsexg 2799  opeqsn 2809  opthwiener 2814  opabid 2817  brabg 2825  opabn0 2831  pwunss 2833  pwundif 2835  dfid3 2843  pocl 2851  sotric 2867  so 2871  uniuni 2887  reuxfr2 2910  reuxfr 2911  elpwun 2918  iunpw 2921  dffr2 2926  fr3nr 2933  dfepfr 2939  dfwe2 2942  wefrc 2950  ordtri3or 2986  ordtri2 2989  onintrab2 3021  elsuci 3042  elsucg 3043  sucel 3049  sucid 3058  ordtri2or 3084  ordzsl 3123  onzsl 3124  dflim4 3126  on0eqelt 3131  snsn0non 3132  findsg 3164  tfindsg 3169  elxp 3209  opelxp 3221  brxp 3222  rexxp 3226  ralxpf 3227  opthprc 3228  xpundi 3232  xpundir 3233  xp0r 3246  reluni 3272  relop 3282  opelco 3295  brco 3296  elcnv 3300  elcnv2 3301  eldm2 3315  dmun 3324  dmin 3325  dmi 3333  dmcoss 3370  dmcosseq 3372  rncoeq 3374  resiexg 3403  dfima3 3413  elima2 3416  elima3 3417  imai 3424  imasng 3431  cotr 3443  cnvsym 3444  asymref 3446  asymref2 3447  intirr 3448  cnvopab 3452  cnvsn 3456  elxp4 3460  elxp5 3461  imainss 3470  cnvxp 3471  dfrel2 3492  dfrel3 3496  cores 3506  imaco 3508  coi1 3517  coass 3519  relssdr 3520  cnvpo 3529  dffun2 3533  dffun3 3534  dffun4 3535  dffun5 3536  dffun6 3546  dffun8 3548  funopab 3555  funun 3561  funcnv 3564  fun2cnv 3566  fncnv 3568  fun11 3569  fununi 3570  funcnvuni 3571  imadif 3581  funimaexg 3582  isarep1 3584  fnopabg 3622  fnopab2g 3623  fun 3648  fcoi1 3652  fcoi2 3653  fcnvres 3655  fconst 3665  f11 3671  funforn 3685  f1o2 3700  f1ocnv 3708  ffoss 3718  f11o 3719  f1o00 3721  fo00 3722  fv2 3727  elfv 3729  fv3 3740  tz6.12-1 3743  nfvres 3755  fvopab5 3800  dff3 3825  dffo3 3826  dffo5 3828  ffnfvf 3836  fopabfv 3838  fsn2 3843  fconst3 3857  fconst4 3858  funfvima 3859  imaiun 3871  abexssex 3879  f1fv 3881  f1fvf 3882  isoini 3907  tfrlem3 3920  tfrlem7 3924  tfrlem9 3926  dfrdg2 3940  tz7.48lem 3962  tz7.48-2 3964  dfoprab2 3998  dmoprab 4009  rnoprab 4011  resoprab 4016  ffnoprval 4021  fnoprval 4024  foprval 4025  oprabex3 4029  oprabval3 4037  oprabval6g 4039  fooprval 4044  ndmoprdistr 4056  1st2val 4102  2nd2val 4103  2ndconst 4104  curry1 4105  dfopab2 4120  dfoprab3 4121  dfoprab5 4122  foprab2 4126  el1o 4153  oarec 4203  oeordi 4221  oaabs 4259  dfer2 4269  eqerlem 4277  erdisj 4293  elqs 4297  ecid 4307  qsid 4308  brecop 4313  ecopoprsym 4317  th3qlem1 4321  mapval2 4342  elpm 4343  elpm2 4344  mapsn 4352  ixpeq2 4362  domen 4386  isfi 4389  en1 4433  2dom 4434  xpsnen 4442  xpcomen 4446  xpassen 4448  pw2en 4453  sbthlem9 4462  sdomdomtr 4476  pwuninel 4493  2pwuninel 4494  xpen 4495  mapxpen 4502  xpmapenlem5 4507  ssenen 4511  nneneq 4519  php 4520  0sdom1dom 4532  unfilem1 4562  abfii2 4580  supmo 4592  zfreg2 4613  inf2 4624  inf3lem2 4630  axinf2 4640  zfinf 4642  trcl 4662  zfregs 4664  setind2 4666  tz9.12lem1 4676  tz9.12lem3 4678  rankel 4697  rankval3 4698  unbndrank 4700  rankun 4708  scottexs 4735  scott0s 4736  cplem1 4737  bnd2 4741  kardex 4742  karden 4743  aceq1 4746  aceq2 4748  aceq3lem 4749  aceq3 4750  aceq4 4751  aceq5lem1 4752  aceq5lem2 4753  aceq5lem3 4754  aceq5lem4 4755  aceq5lem5 4756  aceq6b 4759  ac6n 4774  ac9s 4781  kmlem3 4784  kmlem4 4785  kmlem7 4788  kmlem8 4789  kmlem9 4790  kmlem13 4794  kmlem14 4795  kmlem15 4796  aceqkm 4798  zorn2lem6 4810  brdom7disj 4821  brdom6disj 4822  card1 4850  sucxpdom 4864  iscard 4871  iscard2 4872  alephord2 4894  alephislim 4901  cardaleph 4903  alephval3 4921  cf0 4929  cfeq0 4933  cfsuc 4934  cdaen 4943  cdadom1 4952  elni 5023  ltexpi 5048  ltsopq 5094  genpv 5121  genpn0 5125  genpass 5131  1pr 5136  addcompr 5142  mulcompr 5144  distrlem1pr 5146  distrlem5pr 5150  prlem934b 5157  reclem1pr 5175  reclem2pr 5176  suplem1pr 5180  ltsosr 5222  ltasr 5228  mappsrpr 5237  map2psrpr 5239  suppsr3 5243  opelcn 5267  elreal 5269  axaddopr 5284  axmulopr 5285  axicn 5289  axrnegex 5302  axrrecex 5303  pre-axmulgt0 5309  pre-axsup 5310  subadd2 5392  neg11 5425  1re 5454  ltxrltt 5519  xrlenltt 5520  leloet 5537  xrleloet 5576  xrrebndt 5587  ltadd1 5610  leadd2 5612  addgt0 5617  ltneg 5622  ltnegcon2 5624  msqgt0 5632  msq0 5714  rec11i 5786  divmul24t 5792  halfpos 5913  infm3 6063  infmsup 6077  arch 6080  xrinfmss 6088  supxrre 6092  elnnz 6154  elznn0nn 6157  elznn0 6158  elznn 6159  elnn0nn 6180  elnnnn0 6181  zltp1let 6190  uzwo3 6227  zmin 6228  elq 6265  ralrp 6297  icounlem 6420  snunioolem 6422  raluz2 6451  rexuz2 6453  nnwof 6467  nnwos 6468  subsq0 6656  nn0le2msqt 6671  nn0opth2 6675  inelr 6743  replimt 6769  abslt 6882  absle 6883  cau4i 6925  cau5 6926  cvg3 6930  bcpasc 6976  dffsum 7005  csbfsum 7034  clm4 7087  climunii 7105  climeu 7107  climshft2 7113  cvgcmp3cetlem1 7195  cvgcmp3cetlem2 7196  mulc1cncf 7286  ef1tllem 7388  eirrlem1 7396  ruclem1 7518  ruclem3 7520  ruclem8 7525  infxpidmlem6 7565  infxpidmlem7 7566  infxpidmlem9 7568  infxpidmlem12 7571  infmap2lem1 7588  infmap2lem2 7589  alephsuc3 7594  isbasis2g 7618  tgval2t 7623  tgval3t 7631  tgss3t 7644  basgent 7646  clsval2 7689  elcls 7708  ntreq0 7712  islp2 7751  islpi 7753  cncnplem4 7781  sncld 7791  blrn2 7846  cncfmet 7909  metcn4 7975  fsumcnlem 7993  bcthlem7 8009  bcthlem29 8031  bcthlem32 8034  grpidinvlem3 8054  sspval 8385  isphg 8479  isph 8484  siii 8516  ishl 8594  spwmo 8659  spwpr2 8661  pilem1 8673  sincosq1lem 8705  cosh111lem1 8716  cosh111lem3 8718  efifolem4 8727  effoi 8747  grothinf 8783  grothprimlem 8784  grothprim 8785  avril1 8786  h2hcau 8851  axhcompl 8870  hvsubadd 8935  normsub0 9004  bcsALT 9048  hhcmpl 9071  hlimunii 9110  chcmh 9115  norm1ex 9124  elch0 9128  hhsssh2 9142  pjthlem1 9221  omlsilem 9246  pjoc2 9273  chsscon1 9387  chsscon2 9388  spanun 9469  h1deot 9474  h1det 9475  elspansn 9483  cmcm4 9540  cmbr3 9545  cmbr4 9546  osumlem5 9584  osumcor2 9592  5oalem7 9607  3oalem3 9611  pjss2 9627  mayete3 9675  cnvadj 9818  nmopunt 9941  nmcopexlem1 9953  lncnopbd 9968  nmcfnexlem1 9982  riesz2t 10001  nmopcoadj0 10038  bra11 10043  pjnmop 10077  pjssdif1 10105  pjin2 10124  pjin3 10125  pjclem1 10126  strlem1 10180  cvbr2t 10213  cvnbtwn3t 10218  cvnbtwn4t 10219  mdsl2b 10253  mdsldmd1 10261  elat2 10270  chrelat2 10295  chrelat4 10303  atoml 10312  irred 10324  mdsymlem6 10338  mdsymlem8 10340  sumdmdi 10345  dmdbr5at 10352  cdj3 10371  elghom 10387  ghomgrpilem2 10389  cayleylem2 10413  cayleylem3 10414  19.41vvvv 10438  eeeeanv 10439  r19.3rzvb 10440  ntunte 10442  ficli 10470  bsi 10489  hmeogrp 10532  subsp 10548  rcfpfillem2 10572  ishoma 10694  ismonc 10721  blkssatm 10746

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain