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  1580  falnanfal  1583  had0  1603  nic-axALT  1673  equsexvw  2003  sbiedvw  2094  sbievw2  2097  cbvsbv  2099  sbal  2168  sbco4OLD  2174  sb6a  2257  sbiedw  2315  sbied  2506  sbidm  2513  mo  2563  2mosOLD  2648  2eu6  2655  cbvab  2806  nabbib  3034  2ralorOLD  3219  rexcom4a  3277  abv  3476  ceqsex  3514  ceqsexv  3516  spc2ed  3585  clel2g  3643  2reuswap  3736  2reuswap2  3737  2reu5  3748  2rmoswap  3751  nfcdeq  3767  sbcid  3789  sbcco2  3799  sbc7  3804  sbcie2g  3813  eqsbc1  3819  sbcralt  3854  cbvralcsf  3923  cbvrabcsf  3926  abss  4045  ssab  4046  raldifb  4131  difrab  4300  euelss  4314  vn0  4327  sbccsb  4418  vdif0  4451  difrab0eq  4452  ssunsn2  4809  sspr  4817  sstp  4818  uniintsn  4967  brab1  5173  unopab  5206  axrep5  5269  axrep6OLD  5271  intexab  5328  reusv2lem4  5383  reusv2  5385  el  5424  wefrc  5661  eliunxp  5830  ralxp  5834  rexxp  5835  opelco  5864  reldm0  5920  resieq  5990  iss  6035  imai  6074  cnvsymOLDOLD  6116  intasym  6117  asymref  6118  codir  6122  poirr2  6126  xpdifid  6170  rninxp  6181  dfpo2  6298  frpoins2fg  6346  tz6.26OLD  6350  wfis2fgOLD  6359  ordelord  6387  ordtri3  6401  dffun3OLD  6557  funopg  6581  fin  6769  f1cnvcnv  6794  funimass4  6954  fnressn  7159  resoprab  7534  mpo2eqb  7548  elrnmpores  7554  ov6g  7580  imaeqexov  7654  imaeqalov  7655  offval  7689  uniuni  7765  dfwe2  7777  orduniorsuc  7833  tfinds2  7868  dfopab2  8060  dfoprab3s  8061  fmpox  8075  fparlem1  8120  fparlem2  8121  ralxp3f  8145  frpoins3xpg  8148  brtpos0  8241  dftpos3  8252  tpostpos  8254  dfrecs3  8395  dfrecs3OLD  8396  tz7.48lem  8464  omeu  8606  ercnv  8749  ixp0  8954  xpcomco  9085  xpassen  9089  php  9230  phpOLD  9242  findcard3  9301  findcard3OLD  9302  ixpfi2  9373  dfsup2  9467  sup0riota  9488  card2on  9577  infeq5i  9659  cnfcom3lem  9726  ssttrcl  9738  ttrcltr  9739  ttrclss  9743  frins2f  9776  r1elss  9829  rankxplim  9902  scott0s  9911  aceq1  10140  dfac5lem1  10146  dfac5lem2  10147  kmlem3  10176  kmlem8  10181  kmlem16  10189  djuinf  10212  cflemOLD  10269  cf0  10274  alephval2  10595  fpwwe2lem7  10660  fpwwe2lem11  10664  rankcf  10800  r1tskina  10805  wfgru  10839  genpass  11032  psslinpr  11054  ltpsrpr  11132  addeq0  11669  infm3  12210  nnwos  12940  ioo0  13395  ico0  13416  ioc0  13417  icc0  13418  elfz2nn0  13641  elfzmlbp  13662  sqeqori  14236  hashgt12el  14444  hashgt12el2  14445  cshwidxmod  14824  clim0  15525  divalglem6  16418  ncoprmlnprm  16748  pceu  16867  prmreclem2  16938  cshwshash  17125  xpscf  17586  acsfn2  17682  invsym2  17783  cat1  18118  pospo  18364  issubmndb  18792  f1omvdco3  19440  psgnunilem5  19485  efgrelexlemb  19741  gexex  19844  srgrmhm  20192  isdomn3  20688  isdomn4r  20692  lssne0  20922  islindf4  21825  opsrtoslem1  22046  opsrtoslem2  22047  mdetunilem8  22592  cpmatmcllem  22691  pmatcollpw2lem  22750  ntreq0  23050  ordtrest2lem  23176  ist0-3  23318  ist1-2  23320  ist1-3  23322  cmpfi  23381  2ndcctbss  23428  ptbasfi  23554  ptcnplem  23594  hausdiag  23618  hauseqlcld  23619  cnmptcom  23651  txflf  23979  tgphaus  24090  metrest  24500  iccpnfcnv  24930  bcth3  25320  dyadmax  25588  vitalilem2  25599  vitalilem3  25600  mbfimaopnlem  25645  itg2leub  25724  dvres2  25902  ellogdm  26636  reasinsin  26894  leibpilem2  26939  ftalem3  27073  dchreq  27257  bdayimaon  27693  noetainflem4  27740  cuteq1  27833  addsprop  27964  sleadd1  27977  negsprop  28022  mulsprop  28111  mulsuniflem  28130  addsdilem1  28132  addsdilem2  28133  mulsasslem1  28144  mulsasslem2  28145  precsexlem10  28195  precsexlem11  28196  legso  28562  outpasch  28718  axcontlem2  28929  incistruhgr  29043  nbgrel  29304  usgr2pth0  29732  rusgrnumwwlkslem  29936  frgr3v  30241  4cycl2vnunb  30256  frgrncvvdeqlem2  30266  lnon0  30764  spansncvi  31618  pjssmii  31647  nmlnopgt0i  31963  largei  32233  cvexchlem  32334  xfree  32410  nmo  32456  reuxfrdf  32457  fpwrelmapffslem  32690  eliccioo  32860  1arithidom  33506  ufdprmidl  33510  qtophaus  33776  ordtrest2NEWlem  33862  ordtconnlem1  33864  xrge0iifcnv  33873  xrge0iifiso  33875  xrge0iifhom  33877  cntnevol  34170  eulerpartlemgh  34321  ballotlem7  34479  signswch  34517  bnj446  34672  bnj563  34698  bnj110  34813  bnj153  34835  bnj864  34877  bnj865  34878  bnj849  34880  bnj929  34891  bnj1110  34937  fineqvac  35052  cusgr3cyclex  35082  derang0  35115  iccllysconn  35196  cvmsss2  35220  satf0op  35323  elmrsubrn  35466  rexxfr3dALT  35585  quad3  35616  axacprim  35648  dftr6  35692  elintfv  35706  opelco3  35716  elima4  35717  setinds2f  35721  elpotr  35723  wzel  35766  elfuns  35857  dfiota3  35865  brimg  35879  imagesset  35895  lineunray  36089  ellines  36094  hfninf  36128  in-ax8  36166  ss-ax8  36167  bj-elabtru  36816  bj-snglc  36911  bj-mpomptALT  37061  bj-elid7  37113  bj-imdirco  37132  nlpineqsn  37350  curf  37546  tan2h  37560  poimirlem26  37594  poimirlem27  37595  poimirlem30  37598  poimirlem32  37600  poimir  37601  ovoliunnfl  37610  voliunnfl  37612  ftc1anc  37649  inixp  37676  heibor1lem  37757  csbcom2fi  38076  tsna1  38092  anan  38171  brid  38248  ref5  38255  idinxpssinxp4  38262  iss2  38286  xrninxp  38334  cossssid3  38411  dmqs1cosscnvepreseq  38604  disjxrnres5  38689  islshpat  38959  lkr0f  39036  lshpsmreu  39051  cvrnbtwn4  39221  ishlat2  39295  islvol5  39522  tendoeq2  40717  dibelval3  41090  mapdpglem3  41618  hdmapglem7a  41870  4rexfrabdioph  42754  dford4  42986  fgraphopab  43160  onsupmaxb  43196  tfsconcatlem  43294  ifpim123g  43458  ifpbibib  43468  rp-isfinite6  43476  elrncard  43495  undmrnresiss  43562  cnvssco  43564  iunrelexpuztr  43677  dffrege115  43936  brco2f1o  43990  ntrneiiso  44049  ismnuprim  44258  undisjrab  44270  radcnvrat  44278  opelopab4  44516  2sb5nd  44525  un2122  44755  uunT12p4  44768  2sb5ndVD  44875  2sb5ndALT  44897  ndisj2  45001  ssabf  45050  abssf  45062  fourierdlem42  46109  smflimlem4  46734  aiotaexaiotaiota  47052  ndmaovcom  47163  dmafv2rnb  47187  afv2ndeffv0  47218  0nelsetpreimafv  47323  usgrexmpl2nb0  47936  usgrexmpl2nb1  47937  gpg5nbgrvtx03starlem1  47970  gpg5nbgrvtx03starlem2  47971  gpg5nbgrvtx03starlem3  47972  gpg5nbgrvtx13starlem1  47973  gpg5nbgrvtx13starlem2  47974  gpg5nbgrvtx13starlem3  47975  eliunxp2  48196  pgrpgt2nabl  48228  islindeps  48316  lindslinindsimp1  48320  lindslinindsimp2  48326