Theorem bitr2i 265

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 12-Mar-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem bitr2i

Step	Hyp	Ref	Expression
1		bitr2i.1	. . 3 |- ( ph <-> ps )
2		bitr2i.2	. . 3 |- ( ps <-> ch )
3	1, 2	bitri 264	. 2 |- ( ph <-> ch )
4	3	bicomi 214	1 |- ( ch <-> ph )

Syntax hints:   <-> wb 196

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

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  3bitrri  287  3bitr2ri  289  3bitr4ri  293  nan  604  pm4.15  605  pm5.17  932  pm4.83  970  pm5.7  975  3or6  1410  nanim  1452  19.12vvv  1907  19.12vv  2180  cvjust  2617  abbi  2737  necon1abii  2842  nabbi  2896  nrexralim  2999  r19.23v  3023  ralnex2  3045  ralnex3  3046  spc3gv  3298  ralxpxfr2d  3327  sbc8g  3443  ss2rab  3678  difdif  3736  ddif  3742  unass  3770  unss  3787  undi  3874  rabeq0OLD  3960  disj  4017  ssindif0  4031  prneimg  4388  pwsnALT  4429  iinrab2  4583  unopab  4728  axrep5  4776  eqvinop  4955  pwssun  5020  dmun  5331  reldm0  5343  dmres  5419  imadmrn  5476  ssrnres  5572  dmsnn0  5600  coundi  5636  coundir  5637  cnvpo  5673  xpco  5675  fun11  5963  fununi  5964  isarep1  5977  fdmrn  6064  dffv2  6271  fsn  6402  eufnfv  6491  eloprabga  6747  funoprabg  6759  ralrnmpt2  6775  suceloni  7013  funcnvuni  7119  oprabrexex2  7158  fsplit  7282  dfer2  7743  euen1b  8027  xpsnen  8044  1sdom  8163  wemapsolem  8455  zfregcl  8499  zfregclOLD  8501  epfrs  8607  rankbnd  8731  rankbnd2  8732  rankxplim2  8743  rankxplim3  8744  isinfcard  8915  dfac5lem2  8947  dfac5lem5  8950  kmlem14  8985  kmlem15  8986  kmlem16  8987  axdc2lem  9270  axcclem  9279  ac9  9305  ac9s  9315  nnunb  11288  xrrebnd  11999  elfznelfzo  12573  hashfun  13224  hashtpg  13267  rexuz3  14088  imasaddfnlem  16188  isnsgrp  17288  dprd2d2  18443  isnirred  18700  subsubrg2  18807  isdomn2  19299  mdetunilem8  20425  maducoeval2  20446  tgval2  20760  0top  20787  ssntr  20862  uncmp  21206  opnfbas  21646  fbunfip  21673  hausflf2  21802  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALT  21855  metrest  22329  cfilucfil3  23117  ellimc3  23643  plyun0  23953  sinhalfpilem  24215  2lgslem4  25131  dfcgra2  25721  colinearalg  25790  axcontlem5  25848  nb3grprlem2  26283  wlkeq  26529  isspthonpth  26645  clwlkclwwlklem2a4  26898  clwwlksn2  26910  fusgreg2wsp  27200  shlesb1i  28245  pjneli  28582  cnlnssadj  28939  pjin2i  29052  cvnbtwn2  29146  cvnbtwn4  29148  mdsl1i  29180  mdsl2i  29181  hatomistici  29221  cdj3lem3b  29299  iuninc  29379  disjex  29405  disjexc  29406  fpwrelmapffslem  29507  fpwrelmapffs  29509  isarchi2  29739  ismntop  30070  coinfliprv  30544  ballotlem2  30550  ballotlemi1  30564  plymulx  30625  oddprm2  30733  bnj168  30798  bnj153  30950  bnj605  30977  bnj607  30986  bnj986  31024  bnj1090  31047  bnj1128  31058  dfso2  31644  dfpo2  31645  19.12b  31707  soseq  31751  dfom5b  32019  elfuns  32022  dfint3  32059  hfext  32290  trer  32310  bj-abbi  32775  bj-axrep5  32792  wl-nannot  33299  cnambfre  33458  itg2addnclem2  33462  itg2addnc  33464  heiborlem1  33610  lssat  34303  islshpat  34304  lcvnbtwn2  34314  pclfinclN  35236  lhpex2leN  35299  diclspsn  36483  dihmeetlem4preN  36595  dihmeetlem13N  36608  lcdlss  36908  mapd1o  36937  eq0rabdioph  37340  rmspecnonsq  37472  rmxdioph  37583  wopprc  37597  islssfg2  37641  ifpan23  37804  ifpid1g  37839  dfrtrcl5  37936  dfhe3  38069  ntrneikb  38392  ntrneixb  38393  2sbc6g  38616  2sbc5g  38617  iotasbc2  38621  2sb5nd  38776  2sb5ndVD  39146  2sb5ndALT  39168  limsupre2lem  39956  2rexsb  41170  2rexrsb  41171  islindeps  42242