Theorem bitr3i 254

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 205	. 2 |- ( ph <-> ps )
3		bitr3i.2	. 2 |- ( ps <-> ch )
4	2, 3	bitri 252	1 |- ( ph <-> ch )

Syntax hints:   <-> wb 187

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 188

This theorem is referenced by:  3bitrri  275  3bitr3i  278  3bitr3ri  279  xchnxbi  309  ianor  490  orordi  532  orordir  533  anandi  835  anandir  836  trunantru  1481  falnanfal  1485  had0  1502  nic-axALT  1553  sbied  2201  sbidm  2206  sb6a  2241  sbelx  2251  sbco4  2259  mo  2302  2eu6  2354  bm1.1  2403  abeq1iOLD  2550  cbvab  2561  necon1bbiiOLD  2687  nabbi  2756  r19.41v  2978  r19.41  2979  2ralor  2996  rexcom4a  3099  moeq  3244  2reuswap  3271  2reu5  3277  nfcdeq  3293  sbcid  3313  sbcco2  3320  sbc7  3324  sbcie2g  3330  eqsbc3  3336  sbcralt  3369  cbvralcsf  3424  cbvrabcsf  3427  abss  3527  ssab  3528  difrab  3744  euelss  3757  neq0  3769  sbccsb  3818  vdif0  3850  difrab0eq  3851  ssunsn2  4153  sspr  4157  sstp  4158  prsspwOLD  4167  uniintsn  4287  rabasiun  4297  brab1  4463  unopab  4493  axrep5  4535  axsep  4539  intexab  4575  reusv2lem4  4621  reusv2  4623  reuxfrd  4639  wefrc  4840  elvvv  4906  eliunxp  4984  ralxp  4988  rexxp  4989  opelco  5018  reldm0  5064  resieq  5127  iss  5164  imai  5192  cnvsym  5226  intasym  5227  asymref  5228  codir  5232  poirr2  5236  xpdifid  5277  rninxp  5288  tz6.26  5422  wfis2fg  5428  ordelord  5456  dffun3  5604  funopg  5625  fin  5772  f1cnvcnv  5796  funimass4  5924  fnressn  6083  resoprab  6398  mpt22eqb  6411  elrnmpt2res  6416  ov6g  6440  offval  6544  uniuni  6606  dfwe2  6614  orduniorsuc  6663  tfinds2  6696  resiexg  6735  dfopab2  6853  dfoprab3s  6854  fmpt2x  6865  fparlem1  6899  fparlem2  6900  brtpos0  6980  dftpos3  6991  tpostpos  6993  dfrecs3  7091  tz7.48lem  7158  omeu  7286  ercnv  7384  ixp0  7555  xpcomco  7660  xpassen  7664  php  7754  findcard3  7812  ixpfi2  7870  dfsup2  7956  sup0riota  7977  card2on  8067  infeq5i  8139  cnfcom3lem  8205  r1elss  8274  rankxplim  8347  scott0s  8356  aceq1  8544  dfac5lem1  8550  dfac5lem2  8551  kmlem3  8578  kmlem8  8583  kmlem16  8591  cflem  8672  cf0  8677  alephval2  8993  rankcf  9198  r1tskina  9203  wfgru  9237  genpass  9430  psslinpr  9452  ltpsrpr  9529  infm3  10564  nnwos  11222  ioo0  11657  ico0  11678  ioc0  11679  icc0  11680  elfz2nn0  11879  elfzmlbp  11896  sqeqori  12379  hashgt12el  12586  hashgt12el2  12587  cshwidxmod  12886  clim0  13548  divalglem6  14356  isprm2lem  14609  ncoprmlnprm  14655  pceu  14774  prmreclem2  14839  cshwshash  15053  isstruct  15109  xpscf  15450  acsfn2  15547  invsym2  15646  pospo  16197  f1omvdco3  17068  psgnunilem5  17113  efgrelexlemb  17378  gexex  17469  srgrmhm  17747  lssne0  18152  opsrtoslem1  18685  opsrtoslem2  18686  islindf4  19373  mdetunilem8  19621  cpmatmcllem  19719  pmatcollpw2lem  19778  ntreq0  20070  ordtrest2lem  20196  ist0-3  20338  ist1-2  20340  ist1-3  20342  cmpfi  20400  2ndcctbss  20447  ptbasfi  20573  ptcnplem  20613  hausdiag  20637  hauseqlcld  20638  cnmptcom  20670  txflf  20998  tgphaus  21108  metrest  21516  iccpnfcnv  21949  bcth3  22276  volun  22475  dyadmax  22533  vitalilem2  22544  vitalilem3  22545  mbfimaopnlem  22588  itg2leub  22669  dvres2  22844  ellogdm  23561  reasinsin  23799  leibpilem2  23844  ftalem3  23976  dchreq  24163  legso  24621  outpasch  24774  axcontlem2  24972  rusgranumwlklem0  25652  frgra3v  25706  4cycl2vnunb  25721  vdn0frgrav2  25727  vdgn0frgrav2  25728  usg2spot2nb  25769  lnon0  26415  spansncvi  27281  pjssmii  27310  nmlnopgt0i  27626  largei  27896  cvexchlem  27997  xfree  28073  spc2ed  28082  nmo  28097  2reuswap2  28100  fpwrelmapffslem  28302  addeq0  28305  eliccioo  28387  qtophaus  28652  ordtrest2NEWlem  28717  ordtconlem1  28719  xrge0iifcnv  28728  xrge0iifiso  28730  xrge0iifhom  28732  cntnevol  29039  eulerpartlemgh  29200  ballotlemfp1  29313  ballotlem7  29357  ballotlem7OLD  29395  signswch  29439  bnj446  29511  bnj563  29542  bnj110  29658  bnj153  29680  bnj864  29722  bnj865  29723  bnj849  29725  bnj929  29736  bnj1110  29780  derang0  29881  iccllyscon  29962  cvmsss2  29986  elmrsubrn  30147  quad3  30291  axacprim  30323  dftr6  30378  dfpo2  30383  opelco3  30408  elima4  30409  setinds2f  30413  elpotr  30415  frins2fg  30473  wzel  30495  nobndlem1  30567  elfuns  30668  dfiota3  30676  imagesset  30706  lineunray  30900  ellines  30905  hfninf  30939  bj-axrep5  31359  bj-axsep  31360  bj-rexcom4a  31431  bj-snglc  31513  finixpnum  31838  fin2so  31840  tan2h  31845  poimirlem26  31874  poimirlem27  31875  poimirlem30  31878  poimirlem32  31880  poimir  31881  ovoliunnfl  31890  voliunnfl  31892  ftc1anc  31933  inixp  31963  heibor1lem  32049  csbcom2fi  32277  tsna1  32294  islshpat  32496  lkr0f  32573  lshpsmreu  32588  cvrnbtwn4  32758  ishlat2  32832  islvol5  33057  tendoeq2  34254  dibelval3  34628  mapdpglem3  35156  hdmapglem7a  35411  4rexfrabdioph  35554  dford4  35798  isdomn3  35995  fgraphopab  36001  ifpim123g  36058  ifpbibib  36068  iunrelexpuztr  36165  dffrege115  36426  undisjrab  36506  radcnvrat  36515  opelopab4  36770  2sb5nd  36779  un2122  37032  uunT12p4  37045  onfrALTlem5VD  37137  2sb5ndVD  37162  2sb5ndALT  37184  ndisj2  37245  ellimcabssub0  37484  fourierdlem42  37799  fourierdlem42OLD  37800  2rmoswap  38226  ndmaovcom  38327  nnsum4primesodd  38511  nnsum4primesoddALTV  38512  usgra2pth0  38731  eliunxp2  39179  pgrpgt2nabl  39215  islindeps  39310  lindslinindsimp1  39314  lindslinindsimp2  39320