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 223	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3i.2	. 2 ⊢ (𝜓 ↔ 𝜒)
4	2, 3	bitri 275	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  298  3bitr3i  301  3bitr3ri  302  xchnxbi  332  an13  646  anandi  675  anandir  676  orordi  928  orordir  929  ianor  981  trunantru  1583  falnanfal  1586  had0  1606  nic-axALT  1677  equsexvw  2009  sbiedvw  2097  sbievw2  2100  sbal  2160  sb6a  2250  sb56OLD  2270  sbco4  2275  sbiedw  2310  cbvsbv  2360  sbied  2503  sbidm  2510  mo  2560  2mos  2646  2eu6  2653  cbvabwOLD  2808  cbvab  2809  elisset  2816  nabbib  3046  r19.41v  3189  2ralorOLD  3230  r19.41  3261  rexcom4a  3290  abv  3486  ceqsex  3524  ceqsexv  3526  spc2ed  3592  clel2g  3647  2reuswap  3742  2reuswap2  3743  2reu5  3754  2rmoswap  3757  nfcdeq  3773  sbcid  3794  sbcco2  3804  sbc7  3810  sbcie2g  3819  eqsbc1  3826  sbcralt  3866  cbvralcsf  3938  cbvrabcsf  3941  abss  4057  ssab  4058  raldifb  4144  difrab  4308  euelss  4321  vn0  4338  sbccsb  4433  vdif0  4468  difrab0eq  4469  ssunsn2  4830  sspr  4836  sstp  4837  uniintsn  4991  brab1  5196  unopab  5230  axrep5  5291  axrep6  5292  intexab  5339  reusv2lem4  5399  reusv2  5401  el  5437  wefrc  5670  eliunxp  5836  ralxp  5840  rexxp  5841  opelco  5870  reldm0  5926  resieq  5991  iss  6034  imai  6071  cnvsymOLDOLD  6113  intasym  6114  asymref  6115  codir  6119  poirr2  6123  xpdifid  6165  rninxp  6176  dfpo2  6293  frpoins2fg  6343  tz6.26OLD  6347  wfis2fgOLD  6356  ordelord  6384  ordtri3  6398  dffun3OLD  6556  funopg  6580  fin  6769  f1cnvcnv  6795  funimass4  6954  fnressn  7153  resoprab  7523  mpo2eqb  7538  elrnmpores  7543  ov6g  7568  imaeqexov  7642  imaeqalov  7643  offval  7676  uniuni  7746  dfwe2  7758  orduniorsuc  7815  tfinds2  7850  dfopab2  8035  dfoprab3s  8036  fmpox  8050  fparlem1  8095  fparlem2  8096  ralxp3f  8120  frpoins3xpg  8123  brtpos0  8215  dftpos3  8226  tpostpos  8228  dfrecs3  8369  dfrecs3OLD  8370  tz7.48lem  8438  omeu  8582  ercnv  8721  ixp0  8922  xpcomco  9059  xpassen  9063  php  9207  phpOLD  9219  findcard3  9282  findcard3OLD  9283  ixpfi2  9347  dfsup2  9436  sup0riota  9457  card2on  9546  infeq5i  9628  cnfcom3lem  9695  ssttrcl  9707  ttrcltr  9708  ttrclss  9712  frins2f  9745  r1elss  9798  rankxplim  9871  scott0s  9880  aceq1  10109  dfac5lem1  10115  dfac5lem2  10116  kmlem3  10144  kmlem8  10149  kmlem16  10157  djuinf  10180  cflem  10238  cf0  10243  alephval2  10564  fpwwe2lem7  10629  fpwwe2lem11  10633  rankcf  10769  r1tskina  10774  wfgru  10808  genpass  11001  psslinpr  11023  ltpsrpr  11101  addeq0  11634  infm3  12170  nnwos  12896  ioo0  13346  ico0  13367  ioc0  13368  icc0  13369  elfz2nn0  13589  elfzmlbp  13609  sqeqori  14175  hashgt12el  14379  hashgt12el2  14380  cshwidxmod  14750  clim0  15447  divalglem6  16338  ncoprmlnprm  16661  pceu  16776  prmreclem2  16847  cshwshash  17035  xpscf  17508  acsfn2  17604  invsym2  17707  cat1  18044  pospo  18295  issubmndb  18683  f1omvdco3  19312  psgnunilem5  19357  efgrelexlemb  19613  gexex  19716  srgrmhm  20039  lssne0  20554  islindf4  21385  opsrtoslem1  21608  opsrtoslem2  21609  mdetunilem8  22113  cpmatmcllem  22212  pmatcollpw2lem  22271  ntreq0  22573  ordtrest2lem  22699  ist0-3  22841  ist1-2  22843  ist1-3  22845  cmpfi  22904  2ndcctbss  22951  ptbasfi  23077  ptcnplem  23117  hausdiag  23141  hauseqlcld  23142  cnmptcom  23174  txflf  23502  tgphaus  23613  metrest  24025  iccpnfcnv  24452  bcth3  24840  dyadmax  25107  vitalilem2  25118  vitalilem3  25119  mbfimaopnlem  25164  itg2leub  25244  dvres2  25421  ellogdm  26139  reasinsin  26391  leibpilem2  26436  ftalem3  26569  dchreq  26751  bdayimaon  27186  noetainflem4  27233  cuteq1  27324  addsprop  27450  sleadd1  27462  negsprop  27499  mulsprop  27576  mulsuniflem  27594  addsdilem1  27596  addsdilem2  27597  mulsasslem1  27608  mulsasslem2  27609  precsexlem10  27652  precsexlem11  27653  legso  27840  outpasch  27996  axcontlem2  28213  incistruhgr  28329  nbgrel  28587  usgr2pth0  29012  rusgrnumwwlkslem  29213  frgr3v  29518  4cycl2vnunb  29533  frgrncvvdeqlem2  29543  lnon0  30039  spansncvi  30893  pjssmii  30922  nmlnopgt0i  31238  largei  31508  cvexchlem  31609  xfree  31685  nmo  31718  reuxfrdf  31719  fpwrelmapffslem  31945  eliccioo  32085  qtophaus  32805  ordtrest2NEWlem  32891  ordtconnlem1  32893  xrge0iifcnv  32902  xrge0iifiso  32904  xrge0iifhom  32906  cntnevol  33215  eulerpartlemgh  33366  ballotlem7  33523  signswch  33561  bnj446  33717  bnj563  33743  bnj110  33858  bnj153  33880  bnj864  33922  bnj865  33923  bnj849  33925  bnj929  33936  bnj1110  33982  fineqvac  34086  cusgr3cyclex  34116  derang0  34149  iccllysconn  34230  cvmsss2  34254  satf0op  34357  elmrsubrn  34500  quad3  34644  axacprim  34665  dftr6  34710  elintfv  34725  opelco3  34735  elima4  34736  setinds2f  34740  elpotr  34742  wzel  34785  elfuns  34876  dfiota3  34884  brimg  34898  imagesset  34914  lineunray  35108  ellines  35113  hfninf  35147  bj-elabtru  35742  bj-snglc  35839  bj-mpomptALT  35989  bj-elid7  36041  bj-imdirco  36060  nlpineqsn  36278  curf  36455  tan2h  36469  poimirlem26  36503  poimirlem27  36504  poimirlem30  36507  poimirlem32  36509  poimir  36510  ovoliunnfl  36519  voliunnfl  36521  ftc1anc  36558  inixp  36585  heibor1lem  36666  csbcom2fi  36985  tsna1  37001  anan  37082  brid  37164  ref5  37171  idinxpssinxp4  37178  iss2  37202  xrninxp  37251  cossssid3  37328  dmqs1cosscnvepreseq  37521  disjxrnres5  37606  islshpat  37876  lkr0f  37953  lshpsmreu  37968  cvrnbtwn4  38138  ishlat2  38212  islvol5  38439  tendoeq2  39634  dibelval3  40007  mapdpglem3  40535  hdmapglem7a  40787  4rexfrabdioph  41522  dford4  41754  isdomn3  41932  fgraphopab  41938  onsupmaxb  41974  tfsconcatlem  42072  ifpim123g  42237  ifpbibib  42247  rp-isfinite6  42255  elrncard  42274  undmrnresiss  42341  cnvssco  42343  iunrelexpuztr  42456  dffrege115  42715  brco2f1o  42769  ntrneiiso  42828  ismnuprim  43039  undisjrab  43051  radcnvrat  43059  opelopab4  43298  2sb5nd  43307  un2122  43537  uunT12p4  43550  2sb5ndVD  43657  2sb5ndALT  43679  ndisj2  43724  ssabf  43775  abssf  43787  fourierdlem42  44852  smflimlem4  45477  aiotaexaiotaiota  45789  ndmaovcom  45900  dmafv2rnb  45924  afv2ndeffv0  45955  0nelsetpreimafv  46045  eliunxp2  46963  pgrpgt2nabl  46996  islindeps  47088  lindslinindsimp1  47092  lindslinindsimp2  47098