Theorem bitr3i 276

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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  3bitrri  297  3bitr3i  300  3bitr3ri  301  xchnxbi  331  an13  643  anandi  672  anandir  673  orordi  925  orordir  926  ianor  978  trunantru  1580  falnanfal  1583  had0  1607  nic-axALT  1678  equsexvw  2009  sbiedvw  2098  sbievw2  2101  sbal  2161  sb6a  2253  sb56OLD  2273  sbco4  2278  sbiedw  2313  sbiedwOLD  2314  sbied  2507  sbidm  2514  mo  2565  2mos  2651  2eu6  2658  cbvabv  2812  cbvabwOLD  2814  cbvab  2815  nabbi  3046  rexcom4a  3181  r19.41v  3273  r19.41  3274  2ralorOLD  3295  abv  3433  spc2ed  3530  clel2g  3581  2reuswap  3676  2reuswap2  3677  2reu5  3688  2rmoswap  3691  nfcdeq  3707  sbcid  3728  sbcco2  3738  sbc7  3744  sbcie2g  3753  eqsbc1  3760  sbcralt  3801  cbvralcsf  3873  cbvrabcsf  3876  abss  3990  ssab  3991  raldifb  4075  difrab  4239  euelss  4252  vn0  4269  sbccsb  4364  vdif0  4399  difrab0eq  4400  ssunsn2  4757  sspr  4763  sstp  4764  uniintsn  4915  brab1  5118  unopab  5152  axrep5  5211  axrep6  5212  intexab  5258  reusv2lem4  5319  reusv2  5321  wefrc  5574  eliunxp  5735  ralxp  5739  rexxp  5740  opelco  5769  reldm0  5826  resieq  5891  iss  5932  imai  5971  cnvsym  6008  intasym  6009  asymref  6010  codir  6014  poirr2  6018  xpdifid  6060  rninxp  6071  dfpo2  6188  frpoins2fg  6232  tz6.26OLD  6236  wfis2fgOLD  6245  ordelord  6273  ordtri3  6287  dffun3  6429  funopg  6452  fin  6638  f1cnvcnv  6664  funimass4  6816  fnressn  7012  resoprab  7370  mpo2eqb  7384  elrnmpores  7389  ov6g  7414  offval  7520  uniuni  7590  dfwe2  7602  orduniorsuc  7652  tfinds2  7685  dfopab2  7865  dfoprab3s  7866  fmpox  7880  fparlem1  7923  fparlem2  7924  brtpos0  8020  dftpos3  8031  tpostpos  8033  dfrecs3  8174  dfrecs3OLD  8175  tz7.48lem  8242  omeu  8378  ercnv  8477  ixp0  8677  xpcomco  8802  xpassen  8806  php  8897  findcard3  8987  ixpfi2  9047  dfsup2  9133  sup0riota  9154  card2on  9243  infeq5i  9324  cnfcom3lem  9391  frins2f  9442  r1elss  9495  rankxplim  9568  scott0s  9577  aceq1  9804  dfac5lem1  9810  dfac5lem2  9811  kmlem3  9839  kmlem8  9844  kmlem16  9852  djuinf  9875  cflem  9933  cf0  9938  alephval2  10259  fpwwe2lem7  10324  fpwwe2lem11  10328  rankcf  10464  r1tskina  10469  wfgru  10503  genpass  10696  psslinpr  10718  ltpsrpr  10796  addeq0  11328  infm3  11864  nnwos  12584  ioo0  13033  ico0  13054  ioc0  13055  icc0  13056  elfz2nn0  13276  elfzmlbp  13296  sqeqori  13858  hashgt12el  14065  hashgt12el2  14066  cshwidxmod  14444  clim0  15143  divalglem6  16035  ncoprmlnprm  16360  pceu  16475  prmreclem2  16546  cshwshash  16734  xpscf  17193  acsfn2  17289  invsym2  17392  cat1  17728  pospo  17978  issubmndb  18359  f1omvdco3  18972  psgnunilem5  19017  efgrelexlemb  19271  gexex  19369  srgrmhm  19687  lssne0  20127  islindf4  20955  opsrtoslem1  21172  opsrtoslem2  21173  mdetunilem8  21676  cpmatmcllem  21775  pmatcollpw2lem  21834  ntreq0  22136  ordtrest2lem  22262  ist0-3  22404  ist1-2  22406  ist1-3  22408  cmpfi  22467  2ndcctbss  22514  ptbasfi  22640  ptcnplem  22680  hausdiag  22704  hauseqlcld  22705  cnmptcom  22737  txflf  23065  tgphaus  23176  metrest  23586  iccpnfcnv  24013  bcth3  24400  dyadmax  24667  vitalilem2  24678  vitalilem3  24679  mbfimaopnlem  24724  itg2leub  24804  dvres2  24981  ellogdm  25699  reasinsin  25951  leibpilem2  25996  ftalem3  26129  dchreq  26311  legso  26864  outpasch  27020  axcontlem2  27236  incistruhgr  27352  nbgrel  27610  usgr2pth0  28034  rusgrnumwwlkslem  28235  frgr3v  28540  4cycl2vnunb  28555  frgrncvvdeqlem2  28565  lnon0  29061  spansncvi  29915  pjssmii  29944  nmlnopgt0i  30260  largei  30530  cvexchlem  30631  xfree  30707  nmo  30739  reuxfrdf  30740  fpwrelmapffslem  30969  eliccioo  31107  qtophaus  31688  ordtrest2NEWlem  31774  ordtconnlem1  31776  xrge0iifcnv  31785  xrge0iifiso  31787  xrge0iifhom  31789  cntnevol  32096  eulerpartlemgh  32245  ballotlem7  32402  signswch  32440  bnj446  32596  bnj563  32623  bnj110  32738  bnj153  32760  bnj864  32802  bnj865  32803  bnj849  32805  bnj929  32816  bnj1110  32862  fineqvac  32966  cusgr3cyclex  32998  derang0  33031  iccllysconn  33112  cvmsss2  33136  satf0op  33239  elmrsubrn  33382  quad3  33528  axacprim  33548  ralxp3f  33588  dftr6  33624  elintfv  33644  opelco3  33655  elima4  33656  setinds2f  33661  elpotr  33663  ssttrcl  33701  ttrcltr  33702  ttrclss  33706  frpoins3xpg  33714  frpoins3xp3g  33715  xpord3pred  33725  wzel  33745  bdayimaon  33823  noetainflem4  33870  elfuns  34144  dfiota3  34152  brimg  34166  imagesset  34182  lineunray  34376  ellines  34381  hfninf  34415  bj-elabtru  34985  bj-snglc  35086  bj-mpomptALT  35217  bj-elid7  35269  bj-imdirco  35288  nlpineqsn  35506  curf  35682  tan2h  35696  poimirlem26  35730  poimirlem27  35731  poimirlem30  35734  poimirlem32  35736  poimir  35737  ovoliunnfl  35746  voliunnfl  35748  ftc1anc  35785  inixp  35813  heibor1lem  35894  csbcom2fi  36213  tsna1  36229  anan  36306  brid  36369  idinxpssinxp4  36382  iss2  36406  xrninxp  36445  cossssid3  36514  dmqs1cosscnvepreseq  36701  islshpat  36958  lkr0f  37035  lshpsmreu  37050  cvrnbtwn4  37220  ishlat2  37294  islvol5  37520  tendoeq2  38715  dibelval3  39088  mapdpglem3  39616  hdmapglem7a  39868  4rexfrabdioph  40536  dford4  40767  isdomn3  40945  fgraphopab  40951  ifpim123g  41005  ifpbibib  41015  rp-isfinite6  41023  elrncard  41040  undmrnresiss  41101  cnvssco  41103  iunrelexpuztr  41216  dffrege115  41475  brco2f1o  41531  ntrneiiso  41590  ismnuprim  41801  undisjrab  41813  radcnvrat  41821  opelopab4  42060  2sb5nd  42069  un2122  42299  uunT12p4  42312  2sb5ndVD  42419  2sb5ndALT  42441  ndisj2  42488  ssabf  42539  abssf  42551  fourierdlem42  43580  smflimlem4  44196  aiotaexaiotaiota  44473  ndmaovcom  44584  dmafv2rnb  44608  afv2ndeffv0  44639  0nelsetpreimafv  44730  eliunxp2  45557  pgrpgt2nabl  45590  islindeps  45682  lindslinindsimp1  45686  lindslinindsimp2  45692