Theorem bitr3i 251

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

Hypotheses

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

Assertion

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

Proof of Theorem bitr3i

Step	Hyp	Ref	Expression
1		bitr3i.1	. . 3 |- ( ps <-> ph )
2	1	bicomi 202	. 2 |- ( ph <-> ps )
3		bitr3i.2	. 2 |- ( ps <-> ch )
4	2, 3	bitri 249	1 |- ( ph <-> ch )

Syntax hints:   <-> wb 184

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 185

This theorem is referenced by:  3bitrri  272  3bitr3i  275  3bitr3ri  276  xchnxbi  308  ianor  488  orordi  530  orordir  531  anandi  828  anandir  829  trunantru  1425  falnanfal  1428  had0  1458  nic-axALT  1494  sbied  2137  sbidm  2142  sb6a  2178  sbelx  2188  sbco4  2196  mo  2311  2eu6  2369  2eu6OLD  2370  bm1.1  2426  abeq1iOLD  2573  cbvab  2584  necon1bbiiOLD  2708  nabbi  2776  r19.41v  2995  r19.41  2996  2ralor  3013  rexcom4a  3116  moeq  3261  2reuswap  3288  2reu5  3294  nfcdeq  3310  sbcid  3330  sbcco2  3337  sbc7  3341  sbcie2g  3347  eqsbc3  3353  sbcralt  3394  cbvralcsf  3452  cbvrabcsf  3455  abss  3554  ssab  3555  difrab  3757  neq0  3781  sbccsb  3835  vdif0  3872  difrab0eq  3873  ssunsn2  4174  sspr  4178  sstp  4179  prsspwOLD  4188  uniintsn  4309  rabasiun  4319  disjmoOLD  4422  brab1  4482  unopab  4512  axrep5  4553  axsep  4557  intexab  4595  reusv2lem4  4641  reusv2  4643  reuxfrd  4662  wefrc  4863  ordelord  4890  elvvv  5049  eliunxp  5130  ralxp  5134  rexxp  5135  opelco  5164  reldm0  5210  resieq  5274  iss  5311  imai  5339  cnvsym  5371  intasym  5372  asymref  5373  codir  5377  poirr2  5381  xpdifid  5425  rninxp  5436  dffun3  5589  funopg  5610  fin  5755  f1cnvcnv  5779  funimass4  5909  fnressn  6068  resoprab  6383  mpt22eqb  6396  elrnmpt2res  6401  ov6g  6425  offval  6532  uniuni  6594  dfwe2  6602  orduniorsuc  6650  tfinds2  6683  resiexg  6721  dfopab2  6839  dfoprab3s  6840  fmpt2x  6851  fparlem1  6885  fparlem2  6886  brtpos0  6964  dftpos3  6975  tpostpos  6977  tz7.48lem  7108  omeu  7236  ercnv  7334  ixp0  7504  xpcomco  7609  xpassen  7613  php  7703  findcard3  7765  ixpfi2  7820  dfsup2  7904  card2on  7983  infeq5i  8056  cnfcom3lem  8150  cnfcom3lemOLD  8158  r1elss  8227  rankxplim  8300  scott0s  8309  aceq1  8501  dfac5lem1  8507  dfac5lem2  8508  kmlem3  8535  kmlem8  8540  kmlem16  8548  cflem  8629  cf0  8634  alephval2  8950  rankcf  9158  r1tskina  9163  wfgru  9197  genpass  9390  psslinpr  9412  ltpsrpr  9489  infm3  10509  nnwos  11159  ioo0  11564  ico0  11585  ioc0  11586  icc0  11587  elfz2nn0  11779  elfzmlbp  11796  sqeqori  12261  hashgt12el  12462  hashgt12el2  12463  cshwidxmod  12755  clim0  13310  divalglem6  14037  isprm2lem  14205  pceu  14351  prmreclem2  14416  cshwshash  14570  isstruct  14623  xpscf  14944  acsfn2  15041  invsym2  15138  pospo  15581  f1omvdco3  16452  psgnunilem5  16497  efgrelexlemb  16746  gexex  16837  srgrmhm  17165  lssne0  17575  opsrtoslem1  18126  opsrtoslem2  18127  islindf4  18850  mdetunilem8  19098  cpmatmcllem  19196  pmatcollpw2lem  19255  ntreq0  19555  ordtrest2lem  19681  ist0-3  19823  ist1-2  19825  ist1-3  19827  cmpfi  19885  2ndcctbss  19933  ptbasfi  20059  ptcnplem  20099  hausdiag  20123  hauseqlcld  20124  cnmptcom  20156  txflf  20484  tgphaus  20592  metrest  21004  iccpnfcnv  21421  bcth3  21747  volun  21932  dyadmax  21984  vitalilem2  21995  vitalilem3  21996  mbfimaopnlem  22039  itg2leub  22118  dvres2  22293  ellogdm  22996  reasinsin  23203  leibpilem2  23248  ftalem3  23324  dchreq  23509  legso  23961  axcontlem2  24244  rusgranumwlklem0  24924  frgra3v  24978  4cycl2vnunb  24993  vdn0frgrav2  24999  vdgn0frgrav2  25000  usg2spot2nb  25041  lnon0  25689  spansncvi  26546  pjssmii  26575  nmlnopgt0i  26892  largei  27162  cvexchlem  27263  xfree  27339  spc2ed  27348  nmo  27360  2reuswap2  27363  fpwrelmapffslem  27531  addeq0  27534  eliccioo  27604  qtophaus  27816  ordtrest2NEWlem  27881  ordtconlem1  27883  xrge0iifcnv  27892  xrge0iifiso  27894  xrge0iifhom  27896  cntnevol  28176  eulerpartlemgh  28294  ballotlemfp1  28407  ballotlem7  28451  signswch  28495  derang0  28590  iccllyscon  28672  cvmsss2  28696  elmrsubrn  28857  quad3  29001  axacprim  29056  dftr6  29154  dfpo2  29159  opelco3  29183  elima4  29184  setinds2f  29186  elpotr  29188  tz6.26  29260  wfis2fg  29266  frins2fg  29302  wzel  29355  nobndlem1  29427  elfuns  29540  dfiota3  29548  imagesset  29578  lineunray  29772  ellines  29777  hfninf  29818  finixpnum  30013  fin2so  30015  tan2h  30022  ovoliunnfl  30031  voliunnfl  30033  ftc1anc  30073  inixp  30194  heibor1lem  30280  csbcom2fi  30509  tsna1  30526  4rexfrabdioph  30706  dford4  30946  isdomn3  31140  fgraphopab  31146  undisjrab  31162  radcnvrat  31171  ellimcabssub0  31531  fourierdlem42  31820  2rmoswap  32027  ndmaovcom  32128  usgra2pth0  32193  eliunxp2  32656  pgrpgt2nabl  32692  islindeps  32789  lindslinindsimp1  32793  lindslinindsimp2  32799  opelopab4  33057  2sb5nd  33066  un2122  33320  uunT12p4  33333  onfrALTlem5VD  33418  2sb5ndVD  33443  2sb5ndALT  33465  bnj446  33502  bnj563  33533  bnj110  33649  bnj153  33671  bnj864  33713  bnj865  33714  bnj849  33716  bnj929  33727  bnj1110  33771  bj-axrep5  34126  bj-axsep  34127  bj-rexcom4a  34194  bj-snglc  34275  islshpat  34482  lkr0f  34559  lshpsmreu  34574  cvrnbtwn4  34744  ishlat2  34818  islvol5  35043  tendoeq2  36240  dibelval3  36614  mapdpglem3  37142  hdmapglem7a  37397