Theorem bitr3i 269

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

Hypotheses

Ref	Expression
bitr3i.1	⊢ (𝜓 ↔ 𝜑)
bitr3i.2	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
bitr3i	⊢ (𝜑 ↔ 𝜒)

Proof of Theorem bitr3i

Step	Hyp	Ref	Expression
1		bitr3i.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	bicomi 216	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3i.2	. 2 ⊢ (𝜓 ↔ 𝜒)
4	2, 3	bitri 267	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 198

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 199

This theorem is referenced by:  3bitrri  290  3bitr3i  293  3bitr3ri  294  xchnxbi  324  an12  633  anandi  664  anandir  665  orordi  913  orordir  914  ianor  965  trunantru  1549  falnanfal  1552  had0  1568  nic-axALT  1638  sbievw2  2044  sb6a  2186  sb56  2207  sbco4  2414  sbied  2470  sbidm  2477  sbal  2500  sbiedALT  2542  mo  2580  eu6OLDOLD  2594  2mos  2682  2eu6  2690  cbvabv  2905  cbvab  2906  nabbi  3067  rexcom4a  3192  r19.41v  3283  r19.41  3284  2ralor  3305  spc2ed  3515  2reuswap  3644  2reuswap2  3645  2reu5  3653  2rmoswap  3656  nfcdeq  3672  sbcid  3693  sbcco2  3700  sbc7  3704  sbcie2g  3710  eqsbc3  3716  eqsbc3OLD  3717  sbcralt  3753  cbvralcsf  3815  cbvrabcsf  3818  abss  3925  ssab  3926  raldifb  4006  difrab  4159  euelss  4172  sbccsb  4264  vdif0  4296  difrab0eq  4297  ssunsn2  4631  sspr  4637  sstp  4638  uniintsn  4783  brab1  4974  unopab  5004  axrep5  5052  axsep  5056  intexab  5095  reusv2lem4  5152  reusv2  5154  reuxfrd  5171  wefrc  5398  eliunxp  5555  ralxp  5559  rexxp  5560  opelco  5589  reldm0  5639  resieq  5707  iss  5746  imai  5780  cnvsym  5812  intasym  5813  asymref  5814  codir  5818  poirr2  5822  xpdifid  5863  rninxp  5874  tz6.26  6015  wfis2fg  6021  ordelord  6049  ordtri3  6063  dffun3  6197  funopg  6220  fin  6386  f1cnvcnv  6411  funimass4  6558  fnressn  6742  resoprab  7085  mpo2eqb  7098  elrnmpores  7103  ov6g  7127  offval  7233  uniuni  7300  dfwe2  7311  orduniorsuc  7360  tfinds2  7393  dfopab2  7557  dfoprab3s  7558  fmpox  7572  fparlem1  7614  fparlem2  7615  brtpos0  7701  dftpos3  7712  tpostpos  7714  dfrecs3  7812  tz7.48lem  7879  omeu  8011  ercnv  8109  ixp0  8291  xpcomco  8402  xpassen  8406  php  8496  findcard3  8555  ixpfi2  8616  dfsup2  8702  sup0riota  8723  card2on  8812  infeq5i  8892  cnfcom3lem  8959  r1elss  9028  rankxplim  9101  scott0s  9110  aceq1  9336  dfac5lem1  9342  dfac5lem2  9343  kmlem3  9371  kmlem8  9376  kmlem16  9384  djuinf  9411  cflem  9465  cf0  9470  alephval2  9791  fpwwe2lem8  9856  fpwwe2lem12  9860  rankcf  9996  r1tskina  10001  wfgru  10035  genpass  10228  psslinpr  10250  ltpsrpr  10328  addeq0  10863  infm3  11400  nnwos  12128  ioo0  12578  ico0  12599  ioc0  12600  icc0  12601  elfz2nn0  12813  elfzmlbp  12833  sqeqori  13390  hashgt12el  13595  hashgt12el2  13596  cshwidxmod  14026  clim0  14723  divalglem6  15608  ncoprmlnprm  15923  pceu  16038  prmreclem2  16108  cshwshash  16293  xpscfcda  16700  xpscf  16703  acsfn2  16805  invsym2  16904  pospo  17454  f1omvdco3  18351  psgnunilem5  18396  psgnunilem5OLD  18397  efgrelexlemb  18649  gexex  18742  srgrmhm  19022  lssne0  19457  opsrtoslem1  19990  opsrtoslem2  19991  islindf4  20700  mdetunilem8  20948  cpmatmcllem  21046  pmatcollpw2lem  21105  ntreq0  21405  ordtrest2lem  21531  ist0-3  21673  ist1-2  21675  ist1-3  21677  cmpfi  21736  2ndcctbss  21783  ptbasfi  21909  ptcnplem  21949  hausdiag  21973  hauseqlcld  21974  cnmptcom  22006  txflf  22334  tgphaus  22444  metrest  22853  iccpnfcnv  23267  bcth3  23653  dyadmax  23918  vitalilem2  23929  vitalilem3  23930  mbfimaopnlem  23975  itg2leub  24054  dvres2  24229  ellogdm  24939  reasinsin  25191  leibpilem2  25237  ftalem3  25370  dchreq  25552  legso  26103  outpasch  26259  axcontlem2  26470  incistruhgr  26583  nbgrel  26841  usgr2pth0  27270  rusgrnumwwlkslem  27491  frgr3v  27825  4cycl2vnunb  27840  frgrncvvdeqlem2  27850  lnon0  28368  spansncvi  29226  pjssmii  29255  nmlnopgt0i  29571  largei  29841  cvexchlem  29942  xfree  30018  nmo  30052  fpwrelmapffslem  30245  eliccioo  30378  qtophaus  30777  ordtrest2NEWlem  30842  ordtconnlem1  30844  xrge0iifcnv  30853  xrge0iifiso  30855  xrge0iifhom  30857  cntnevol  31165  eulerpartlemgh  31314  ballotlem7  31472  signswch  31510  bnj446  31668  bnj563  31695  bnj110  31810  bnj153  31832  bnj864  31874  bnj865  31875  bnj849  31877  bnj929  31888  bnj1110  31932  derang0  32034  iccllysconn  32115  cvmsss2  32139  satf0op  32220  elmrsubrn  32320  quad3  32466  axacprim  32486  dftr6  32539  dfpo2  32544  elintfv  32560  opelco3  32571  elima4  32572  setinds2f  32577  elpotr  32579  frpoins2fg  32636  frins2fg  32643  wzel  32665  bdayimaon  32751  elfuns  32930  dfiota3  32938  brimg  32952  imagesset  32968  lineunray  33162  ellines  33167  hfninf  33201  bj-axrep5  33655  bj-axsep  33656  bj-snglc  33832  bj-mpomptALT  33953  nlpineqsn  34163  curf  34344  tan2h  34358  poimirlem26  34392  poimirlem27  34393  poimirlem30  34396  poimirlem32  34398  poimir  34399  ovoliunnfl  34408  voliunnfl  34410  ftc1anc  34449  inixp  34478  heibor1lem  34562  csbcom2fi  34883  tsna1  34899  anan  34976  brid  35041  idinxpssinxp4  35054  iss2  35080  xrninxp  35118  cossssid3  35187  dmqs1cosscnvepreseq  35374  islshpat  35631  lkr0f  35708  lshpsmreu  35723  cvrnbtwn4  35893  ishlat2  35967  islvol5  36193  tendoeq2  37388  dibelval3  37761  mapdpglem3  38289  hdmapglem7a  38541  sn-axrep  38585  4rexfrabdioph  38825  dford4  39056  isdomn3  39234  fgraphopab  39240  ifpim123g  39296  ifpbibib  39306  undmrnresiss  39360  cnvssco  39362  iunrelexpuztr  39461  dffrege115  39721  brco2f1o  39779  ntrneiiso  39838  ismnuprim  40039  undisjrab  40088  radcnvrat  40096  opelopab4  40338  2sb5nd  40347  un2122  40577  uunT12p4  40590  2sb5ndVD  40697  2sb5ndALT  40719  ndisj2  40766  ssabf  40820  abssf  40833  fourierdlem42  41895  smflimlem4  42511  aiotaexaiotaiota  42728  ndmaovcom  42840  dmafv2rnb  42864  afv2ndeffv0  42895  eliunxp2  43776  pgrpgt2nabl  43810  islindeps  43905  lindslinindsimp1  43909  lindslinindsimp2  43915