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  647  anandi  676  anandir  677  orordi  928  orordir  929  ianor  983  trunantru  1582  falnanfal  1585  had0  1605  nic-axALT  1675  equsexvw  2006  sbiedvw  2097  sbievw2  2100  cbvsbv  2102  sbal  2171  sbco4OLD  2177  sb6a  2260  sbiedw  2316  sbied  2502  sbidm  2509  mo  2559  2mosOLD  2644  2eu6  2651  cbvab  2802  nabbib  3029  rexcom4a  3260  abv  3446  ceqsex  3483  ceqsexv  3485  spc2ed  3554  clel2g  3612  2reuswap  3703  2reuswap2  3704  2reu5  3715  2rmoswap  3718  nfcdeq  3734  sbcid  3756  sbcco2  3766  sbc7  3771  sbcie2g  3780  eqsbc1  3786  sbcralt  3821  cbvralcsf  3890  cbvrabcsf  3893  abss  4012  ssab  4013  raldifb  4097  difrab  4266  euelss  4280  vn0  4293  sbccsb  4384  vdif0  4417  difrab0eq  4418  ssunsn2  4777  sspr  4785  sstp  4786  uniintsn  4933  brab1  5137  unopab  5169  axrep5  5223  axrep6OLD  5225  intexab  5282  reusv2lem4  5337  reusv2  5339  el  5378  wefrc  5608  eliunxp  5775  ralxp  5779  rexxp  5780  opelco  5809  reldm0  5865  resieq  5936  iss  5981  imai  6020  intasym  6059  asymref  6060  codir  6064  poirr2  6068  xpdifid  6112  rninxp  6123  dfpo2  6239  frpoins2fg  6287  ordelord  6324  ordtri3  6338  funopg  6511  fin  6699  f1cnvcnv  6724  funimass4  6881  fnressn  7086  resoprab  7459  mpo2eqb  7473  elrnmpores  7479  ov6g  7505  imaeqexov  7579  imaeqalov  7580  offval  7614  uniuni  7690  dfwe2  7702  orduniorsuc  7755  tfinds2  7789  dfopab2  7979  dfoprab3s  7980  fmpox  7994  fparlem1  8037  fparlem2  8038  ralxp3f  8062  frpoins3xpg  8065  brtpos0  8158  dftpos3  8169  tpostpos  8171  dfrecs3  8287  tz7.48lem  8355  omeu  8495  ercnv  8638  ixp0  8850  xpcomco  8975  xpassen  8979  php  9111  findcard3  9162  ixpfi2  9229  dfsup2  9323  sup0riota  9345  card2on  9435  infeq5i  9521  cnfcom3lem  9588  ssttrcl  9600  ttrcltr  9601  ttrclss  9605  frins2f  9638  r1elss  9691  rankxplim  9764  scott0s  9773  aceq1  10000  dfac5lem1  10006  dfac5lem2  10007  kmlem3  10036  kmlem8  10041  kmlem16  10049  djuinf  10072  cflemOLD  10129  cf0  10134  alephval2  10455  fpwwe2lem7  10520  fpwwe2lem11  10524  rankcf  10660  r1tskina  10665  wfgru  10699  genpass  10892  psslinpr  10914  ltpsrpr  10992  addeq0  11532  infm3  12073  nnwos  12805  ioo0  13262  ico0  13283  ioc0  13284  icc0  13285  elfz2nn0  13510  elfzmlbp  13531  sqeqori  14113  hashgt12el  14321  hashgt12el2  14322  cshwidxmod  14702  clim0  15405  divalglem6  16301  ncoprmlnprm  16631  pceu  16750  prmreclem2  16821  cshwshash  17008  xpscf  17461  acsfn2  17561  invsym2  17662  cat1  17996  pospo  18241  issubmndb  18705  f1omvdco3  19354  psgnunilem5  19399  efgrelexlemb  19655  gexex  19758  srgrmhm  20133  isdomn3  20623  isdomn4r  20627  lssne0  20877  islindf4  21768  opsrtoslem1  21983  opsrtoslem2  21984  mdetunilem8  22527  cpmatmcllem  22626  pmatcollpw2lem  22685  ntreq0  22985  ordtrest2lem  23111  ist0-3  23253  ist1-2  23255  ist1-3  23257  cmpfi  23316  2ndcctbss  23363  ptbasfi  23489  ptcnplem  23529  hausdiag  23553  hauseqlcld  23554  cnmptcom  23586  txflf  23914  tgphaus  24025  metrest  24432  iccpnfcnv  24862  bcth3  25251  dyadmax  25519  vitalilem2  25530  vitalilem3  25531  mbfimaopnlem  25576  itg2leub  25655  dvres2  25833  ellogdm  26568  reasinsin  26826  leibpilem2  26871  ftalem3  27005  dchreq  27189  bdayimaon  27625  noetainflem4  27672  cuteq1  27771  addsprop  27912  sleadd1  27925  negsprop  27970  mulsprop  28062  mulsuniflem  28081  addsdilem1  28083  addsdilem2  28084  mulsasslem1  28095  mulsasslem2  28096  precsexlem10  28147  precsexlem11  28148  onnolt  28196  bdayn0p1  28287  legso  28570  outpasch  28726  axcontlem2  28936  incistruhgr  29050  nbgrel  29311  usgr2pth0  29736  rusgrnumwwlkslem  29940  frgr3v  30245  4cycl2vnunb  30260  frgrncvvdeqlem2  30270  lnon0  30768  spansncvi  31622  pjssmii  31651  nmlnopgt0i  31967  largei  32237  cvexchlem  32338  xfree  32414  nmo  32459  reuxfrdf  32460  fpwrelmapffslem  32705  eliccioo  32901  1arithidom  33492  ufdprmidl  33496  qtophaus  33839  ordtrest2NEWlem  33925  ordtconnlem1  33927  xrge0iifcnv  33936  xrge0iifiso  33938  xrge0iifhom  33940  cntnevol  34231  eulerpartlemgh  34381  ballotlem7  34539  signswch  34564  bnj446  34719  bnj563  34745  bnj110  34860  bnj153  34882  bnj864  34924  bnj865  34925  bnj849  34927  bnj929  34938  bnj1110  34984  fineqvac  35107  axregs  35113  cusgr3cyclex  35148  derang0  35181  iccllysconn  35262  cvmsss2  35286  satf0op  35389  elmrsubrn  35532  rexxfr3dALT  35651  quad3  35682  axacprim  35719  dftr6  35763  elintfv  35777  opelco3  35787  elima4  35788  setinds2f  35792  elpotr  35794  wzel  35837  elfuns  35928  dfiota3  35936  brimg  35950  imagesset  35966  lineunray  36160  ellines  36165  hfninf  36199  in-ax8  36237  ss-ax8  36238  bj-elabtru  36887  bj-snglc  36982  bj-mpomptALT  37132  bj-elid7  37184  bj-imdirco  37203  nlpineqsn  37421  curf  37617  tan2h  37631  poimirlem26  37665  poimirlem27  37666  poimirlem30  37669  poimirlem32  37671  poimir  37672  ovoliunnfl  37681  voliunnfl  37683  ftc1anc  37720  inixp  37747  heibor1lem  37828  csbcom2fi  38147  tsna1  38163  anan  38242  brid  38319  ref5  38326  idinxpssinxp4  38333  iss2  38351  xrninxp  38403  cossssid3  38485  dmqs1cosscnvepreseq  38679  disjxrnres5  38764  dmqsblocks  38870  islshpat  39035  lkr0f  39112  lshpsmreu  39127  cvrnbtwn4  39297  ishlat2  39371  islvol5  39597  tendoeq2  40792  dibelval3  41165  mapdpglem3  41693  hdmapglem7a  41945  4rexfrabdioph  42810  dford4  43041  fgraphopab  43215  onsupmaxb  43251  tfsconcatlem  43348  ifpim123g  43512  ifpbibib  43522  rp-isfinite6  43530  elrncard  43549  undmrnresiss  43616  cnvssco  43618  iunrelexpuztr  43731  dffrege115  43990  brco2f1o  44044  ntrneiiso  44103  ismnuprim  44306  undisjrab  44318  radcnvrat  44326  opelopab4  44563  2sb5nd  44572  un2122  44801  uunT12p4  44814  2sb5ndVD  44921  2sb5ndALT  44943  ndisj2  45067  ssabf  45116  abssf  45128  fourierdlem42  46166  smflimlem4  46791  aiotaexaiotaiota  47104  ndmaovcom  47215  dmafv2rnb  47239  afv2ndeffv0  47270  modm1p1ne  47380  0nelsetpreimafv  47400  usgrexmpl2nb0  48041  usgrexmpl2nb1  48042  gpg5nbgrvtx03starlem1  48078  gpg5nbgrvtx03starlem2  48079  gpg5nbgrvtx03starlem3  48080  gpg5nbgrvtx13starlem1  48081  gpg5nbgrvtx13starlem2  48082  gpg5nbgrvtx13starlem3  48083  pgnbgreunbgrlem2lem2  48125  gpg5edgnedg  48140  eliunxp2  48344  pgrpgt2nabl  48376  islindeps  48464  lindslinindsimp1  48468  lindslinindsimp2  48474