Theorem bitr3i 277

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 224	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3i.2	. 2 ⊢ (𝜓 ↔ 𝜒)
4	2, 3	bitri 275	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  3bitrri  298  3bitr3i  301  3bitr3ri  302  xchnxbi  332  an13  648  anandi  677  anandir  678  orordi  929  orordir  930  ianor  984  trunantru  1583  falnanfal  1586  had0  1606  nic-axALT  1676  equsexvw  2007  sbiedvw  2101  sbievw2  2104  cbvsbv  2106  sbal  2175  sbco4OLD  2181  sb6a  2266  sbiedw  2322  sbied  2508  sbidm  2515  mo  2566  2mosOLD  2651  2eu6  2658  cbvab  2809  nabbib  3036  rexcom4a  3267  abv  3453  ceqsex  3490  ceqsexv  3491  spc2ed  3556  clel2g  3614  2reuswap  3705  2reuswap2  3706  2reu5  3717  2rmoswap  3720  nfcdeq  3736  sbcid  3758  sbcco2  3768  sbc7  3773  sbcie2g  3782  eqsbc1  3788  sbcralt  3823  cbvralcsf  3892  cbvrabcsf  3895  abss  4015  ssab  4016  raldifb  4102  difrab  4271  euelss  4285  sbccsb  4389  vdif0  4422  difrab0eq  4423  ssunsn2  4784  sspr  4792  sstp  4793  uniintsn  4941  brab1  5147  unopab  5179  axrep5  5233  axrep6OLD  5235  intexab  5292  reusv2lem4  5347  reusv2  5349  el  5388  wefrc  5619  eliunxp  5787  ralxp  5791  rexxp  5792  opelco  5821  reldm0  5878  resieq  5950  iss  5995  imai  6034  intasym  6073  asymref  6074  codir  6078  poirr2  6082  xpdifid  6127  rninxp  6138  dfpo2  6255  frpoins2fg  6303  ordelord  6340  ordtri3  6354  funopg  6527  fin  6715  f1cnvcnv  6740  funimass4  6899  fnressn  7105  resoprab  7478  mpo2eqb  7492  elrnmpores  7498  ov6g  7524  imaeqexov  7598  imaeqalov  7599  offval  7633  uniuni  7709  dfwe2  7721  orduniorsuc  7774  tfinds2  7808  dfopab2  7998  dfoprab3s  7999  fmpox  8013  fparlem1  8056  fparlem2  8057  ralxp3f  8081  frpoins3xpg  8084  brtpos0  8177  dftpos3  8188  tpostpos  8190  dfrecs3  8306  tz7.48lem  8374  omeu  8514  ercnv  8659  ixp0  8873  xpcomco  8999  xpassen  9003  php  9135  findcard3  9187  ixpfi2  9254  dfsup2  9351  sup0riota  9373  card2on  9463  infeq5i  9549  cnfcom3lem  9616  ssttrcl  9628  ttrcltr  9629  ttrclss  9633  setinds2f  9663  frins2f  9669  r1elss  9722  rankxplim  9795  scott0s  9804  aceq1  10031  dfac5lem1  10037  dfac5lem2  10038  kmlem3  10067  kmlem8  10072  kmlem16  10080  djuinf  10103  cflemOLD  10160  cf0  10165  alephval2  10487  fpwwe2lem7  10552  fpwwe2lem11  10556  rankcf  10692  r1tskina  10697  wfgru  10731  genpass  10924  psslinpr  10946  ltpsrpr  11024  addeq0  11564  infm3  12105  nnwos  12832  ioo0  13290  ico0  13311  ioc0  13312  icc0  13313  elfz2nn0  13538  elfzmlbp  13559  sqeqori  14141  hashgt12el  14349  hashgt12el2  14350  cshwidxmod  14730  clim0  15433  divalglem6  16329  ncoprmlnprm  16659  pceu  16778  prmreclem2  16849  cshwshash  17036  xpscf  17490  acsfn2  17590  invsym2  17691  cat1  18025  pospo  18270  issubmndb  18734  f1omvdco3  19382  psgnunilem5  19427  efgrelexlemb  19683  gexex  19786  srgrmhm  20161  isdomn3  20652  isdomn4r  20656  lssne0  20906  islindf4  21797  opsrtoslem1  22014  opsrtoslem2  22015  mdetunilem8  22567  cpmatmcllem  22666  pmatcollpw2lem  22725  ntreq0  23025  ordtrest2lem  23151  ist0-3  23293  ist1-2  23295  ist1-3  23297  cmpfi  23356  2ndcctbss  23403  ptbasfi  23529  ptcnplem  23569  hausdiag  23593  hauseqlcld  23594  cnmptcom  23626  txflf  23954  tgphaus  24065  metrest  24472  iccpnfcnv  24902  bcth3  25291  dyadmax  25559  vitalilem2  25570  vitalilem3  25571  mbfimaopnlem  25616  itg2leub  25695  dvres2  25873  ellogdm  26608  reasinsin  26866  leibpilem2  26911  ftalem3  27045  dchreq  27229  bdayimaon  27665  noetainflem4  27712  cuteq1  27815  addsprop  27958  sleadd1  27971  negsprop  28017  mulsprop  28112  mulsuniflem  28131  addsdilem1  28133  addsdilem2  28134  mulsasslem1  28145  mulsasslem2  28146  precsexlem10  28197  precsexlem11  28198  onnolt  28247  bdayn0p1  28348  legso  28654  outpasch  28810  axcontlem2  29021  incistruhgr  29135  nbgrel  29396  usgr2pth0  29821  rusgrnumwwlkslem  30028  frgr3v  30333  4cycl2vnunb  30348  frgrncvvdeqlem2  30358  lnon0  30856  spansncvi  31710  pjssmii  31739  nmlnopgt0i  32055  largei  32325  cvexchlem  32426  xfree  32502  nmo  32546  reuxfrdf  32547  fpwrelmapffslem  32792  eliccioo  32993  1arithidom  33599  ufdprmidl  33603  qtophaus  33974  ordtrest2NEWlem  34060  ordtconnlem1  34062  xrge0iifcnv  34071  xrge0iifiso  34073  xrge0iifhom  34075  cntnevol  34366  eulerpartlemgh  34516  ballotlem7  34674  signswch  34699  bnj446  34854  bnj563  34880  bnj110  34995  bnj153  35017  bnj864  35059  bnj865  35060  bnj849  35062  bnj929  35073  bnj1110  35119  fineqvac  35253  axregs  35276  cusgr3cyclex  35311  derang0  35344  iccllysconn  35425  cvmsss2  35449  satf0op  35552  elmrsubrn  35695  rexxfr3dALT  35814  quad3  35845  axacprim  35882  dftr6  35926  elintfv  35940  opelco3  35950  elima4  35951  elpotr  35954  wzel  35997  elfuns  36088  dfiota3  36096  brimg  36110  imagesset  36128  lineunray  36322  ellines  36327  hfninf  36361  in-ax8  36399  ss-ax8  36400  bj-elabtru  37050  bj-snglc  37145  bj-mpomptALT  37295  bj-elid7  37347  bj-imdirco  37366  nlpineqsn  37584  curf  37770  tan2h  37784  poimirlem26  37818  poimirlem27  37819  poimirlem30  37822  poimirlem32  37824  poimir  37825  ovoliunnfl  37834  voliunnfl  37836  ftc1anc  37873  inixp  37900  heibor1lem  37981  csbcom2fi  38300  tsna1  38316  anan  38407  brid  38484  ref5  38491  idinxpssinxp4  38498  iss2  38516  raldmqseu  38537  xrninxp  38587  cossssid3  38731  dmqs1cosscnvepreseq  38919  disjxrnres5  39019  dmqsblocks  39139  islshpat  39314  lkr0f  39391  lshpsmreu  39406  cvrnbtwn4  39576  ishlat2  39650  islvol5  39876  tendoeq2  41071  dibelval3  41444  mapdpglem3  41972  hdmapglem7a  42224  4rexfrabdioph  43076  dford4  43307  fgraphopab  43481  onsupmaxb  43517  tfsconcatlem  43614  ifpim123g  43777  ifpbibib  43787  rp-isfinite6  43795  elrncard  43814  undmrnresiss  43881  cnvssco  43883  iunrelexpuztr  43996  dffrege115  44255  brco2f1o  44309  ntrneiiso  44368  ismnuprim  44571  undisjrab  44583  radcnvrat  44591  opelopab4  44828  2sb5nd  44837  un2122  45066  uunT12p4  45079  2sb5ndVD  45186  2sb5ndALT  45208  ndisj2  45332  ssabf  45380  abssf  45392  fourierdlem42  46429  smflimlem4  47054  aiotaexaiotaiota  47376  ndmaovcom  47487  dmafv2rnb  47511  afv2ndeffv0  47542  modm1p1ne  47652  0nelsetpreimafv  47672  usgrexmpl2nb0  48313  usgrexmpl2nb1  48314  gpg5nbgrvtx03starlem1  48350  gpg5nbgrvtx03starlem2  48351  gpg5nbgrvtx03starlem3  48352  gpg5nbgrvtx13starlem1  48353  gpg5nbgrvtx13starlem2  48354  gpg5nbgrvtx13starlem3  48355  pgnbgreunbgrlem2lem2  48397  gpg5edgnedg  48412  eliunxp2  48616  pgrpgt2nabl  48648  islindeps  48735  lindslinindsimp1  48739  lindslinindsimp2  48745