Theorem bitr3i 255

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

Syntax hints:   <-> wb 188

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 189

This theorem is referenced by:  3bitrri  276  3bitr3i  279  3bitr3ri  280  xchnxbi  310  ianor  491  orordi  533  orordir  534  anandi  836  anandir  837  trunantru  1485  falnanfal  1489  had0  1506  nic-axALT  1556  sbied  2237  sbidm  2242  sb6a  2276  sbelx  2286  sbco4  2294  mo  2336  2eu6  2386  bm1.1  2435  cbvab  2573  nabbi  2724  r19.41v  2941  r19.41  2942  2ralor  2959  rexcom4a  3067  moeq  3213  2reuswap  3241  2reu5  3247  nfcdeq  3263  sbcid  3283  sbcco2  3290  sbc7  3294  sbcie2g  3300  eqsbc3  3306  sbcralt  3339  cbvralcsf  3394  cbvrabcsf  3397  abss  3497  ssab  3498  difrab  3716  euelss  3729  neq0  3741  sbccsb  3792  vdif0  3824  difrab0eq  3825  ssunsn2  4130  sspr  4134  sstp  4135  prsspwOLD  4144  uniintsn  4271  rabasiun  4281  brab1  4447  unopab  4477  axrep5  4519  axsep  4523  intexab  4560  reusv2lem4  4606  reusv2  4608  reuxfrd  4624  wefrc  4827  elvvv  4893  eliunxp  4971  ralxp  4975  rexxp  4976  opelco  5005  reldm0  5051  resieq  5114  iss  5151  imai  5179  cnvsym  5213  intasym  5214  asymref  5215  codir  5219  poirr2  5223  xpdifid  5264  rninxp  5275  tz6.26  5410  wfis2fg  5416  ordelord  5444  dffun3  5592  funopg  5613  fin  5761  f1cnvcnv  5785  funimass4  5914  fnressn  6074  resoprab  6389  mpt22eqb  6402  elrnmpt2res  6407  ov6g  6431  offval  6535  uniuni  6597  dfwe2  6605  orduniorsuc  6654  tfinds2  6687  resiexg  6726  dfopab2  6844  dfoprab3s  6845  fmpt2x  6856  fparlem1  6893  fparlem2  6894  brtpos0  6977  dftpos3  6988  tpostpos  6990  dfrecs3  7088  tz7.48lem  7155  omeu  7283  ercnv  7381  ixp0  7552  xpcomco  7659  xpassen  7663  php  7753  findcard3  7811  ixpfi2  7869  dfsup2  7955  sup0riota  7976  card2on  8066  infeq5i  8138  cnfcom3lem  8205  r1elss  8274  rankxplim  8347  scott0s  8356  aceq1  8545  dfac5lem1  8551  dfac5lem2  8552  kmlem3  8579  kmlem8  8584  kmlem16  8592  cflem  8673  cf0  8678  alephval2  8994  rankcf  9199  r1tskina  9204  wfgru  9238  genpass  9431  psslinpr  9453  ltpsrpr  9530  infm3  10565  nnwos  11223  ioo0  11658  ico0  11679  ioc0  11680  icc0  11681  elfz2nn0  11882  elfzmlbp  11899  sqeqori  12383  hashgt12el  12592  hashgt12el2  12593  cshwidxmod  12900  clim0  13563  divalglem6  14371  isprm2lem  14624  ncoprmlnprm  14670  pceu  14789  prmreclem2  14854  cshwshash  15068  isstruct  15124  xpscf  15465  acsfn2  15562  invsym2  15661  pospo  16212  f1omvdco3  17083  psgnunilem5  17128  efgrelexlemb  17393  gexex  17484  srgrmhm  17762  lssne0  18167  opsrtoslem1  18700  opsrtoslem2  18701  islindf4  19389  mdetunilem8  19637  cpmatmcllem  19735  pmatcollpw2lem  19794  ntreq0  20086  ordtrest2lem  20212  ist0-3  20354  ist1-2  20356  ist1-3  20358  cmpfi  20416  2ndcctbss  20463  ptbasfi  20589  ptcnplem  20629  hausdiag  20653  hauseqlcld  20654  cnmptcom  20686  txflf  21014  tgphaus  21124  metrest  21532  iccpnfcnv  21965  bcth3  22292  volun  22491  dyadmax  22549  vitalilem2  22560  vitalilem3  22561  mbfimaopnlem  22604  itg2leub  22685  dvres2  22860  ellogdm  23577  reasinsin  23815  leibpilem2  23860  ftalem3  23992  dchreq  24179  legso  24637  outpasch  24790  axcontlem2  24988  rusgranumwlklem0  25669  frgra3v  25723  4cycl2vnunb  25738  vdn0frgrav2  25744  vdgn0frgrav2  25745  usg2spot2nb  25786  lnon0  26432  spansncvi  27298  pjssmii  27327  nmlnopgt0i  27643  largei  27913  cvexchlem  28014  xfree  28090  spc2ed  28099  nmo  28114  2reuswap2  28117  fpwrelmapffslem  28310  addeq0  28313  eliccioo  28393  qtophaus  28656  ordtrest2NEWlem  28721  ordtconlem1  28723  xrge0iifcnv  28732  xrge0iifiso  28734  xrge0iifhom  28736  cntnevol  29043  eulerpartlemgh  29204  ballotlemfp1  29317  ballotlem7  29361  ballotlem7OLD  29399  signswch  29443  bnj446  29515  bnj563  29546  bnj110  29662  bnj153  29684  bnj864  29726  bnj865  29727  bnj849  29729  bnj929  29740  bnj1110  29784  derang0  29885  iccllyscon  29966  cvmsss2  29990  elmrsubrn  30151  quad3  30295  axacprim  30327  dftr6  30383  dfpo2  30388  opelco3  30413  elima4  30414  setinds2f  30418  elpotr  30420  frins2fg  30478  wzel  30500  nobndlem1  30574  elfuns  30675  dfiota3  30683  imagesset  30713  lineunray  30907  ellines  30912  hfninf  30946  bj-axrep5  31400  bj-axsep  31401  bj-rexcom4a  31472  bj-snglc  31556  bj-mpt2mptALT  31624  finixpnum  31923  fin2so  31925  tan2h  31930  poimirlem26  31959  poimirlem27  31960  poimirlem30  31963  poimirlem32  31965  poimir  31966  ovoliunnfl  31975  voliunnfl  31977  ftc1anc  32018  inixp  32048  heibor1lem  32134  csbcom2fi  32362  tsna1  32379  islshpat  32577  lkr0f  32654  lshpsmreu  32669  cvrnbtwn4  32839  ishlat2  32913  islvol5  33138  tendoeq2  34335  dibelval3  34709  mapdpglem3  35237  hdmapglem7a  35492  4rexfrabdioph  35635  dford4  35878  isdomn3  36075  fgraphopab  36081  ifpim123g  36138  ifpbibib  36148  undmrnresiss  36204  cnvssco  36206  iunrelexpuztr  36305  dffrege115  36568  undisjrab  36648  radcnvrat  36657  opelopab4  36912  2sb5nd  36921  un2122  37171  uunT12p4  37184  onfrALTlem5VD  37276  2sb5ndVD  37301  2sb5ndALT  37323  ndisj2  37383  ellimcabssub0  37691  fourierdlem42  38006  fourierdlem42OLD  38007  2rmoswap  38599  ndmaovcom  38701  nnsum4primesodd  38885  nnsum4primesoddALTV  38886  incistruhgr  39157  usgra2pth0  39656  eliunxp2  40102  pgrpgt2nabl  40138  islindeps  40233  lindslinindsimp1  40237  lindslinindsimp2  40243