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  298  3bitr3i  301  3bitr3ri  302  xchnxbi  332  an13  644  anandi  673  anandir  674  orordi  926  orordir  927  ianor  979  trunantru  1580  falnanfal  1583  had0  1606  nic-axALT  1677  equsexvw  2009  sbiedvw  2097  sbievw2  2100  sbal  2160  sb6a  2251  sb56OLD  2271  sbco4  2276  sbiedw  2311  sbied  2508  sbidm  2515  mo  2566  2mos  2652  2eu6  2659  cbvabv  2812  cbvabwOLD  2814  cbvab  2815  nabbi  3048  rexcom4a  3237  r19.41v  3277  r19.41  3278  2ralorOLD  3298  abv  3444  spc2ed  3541  clel2g  3589  2reuswap  3682  2reuswap2  3683  2reu5  3694  2rmoswap  3697  nfcdeq  3713  sbcid  3734  sbcco2  3744  sbc7  3750  sbcie2g  3759  eqsbc1  3766  sbcralt  3806  cbvralcsf  3878  cbvrabcsf  3881  abss  3995  ssab  3996  raldifb  4080  difrab  4243  euelss  4256  vn0  4273  sbccsb  4368  vdif0  4403  difrab0eq  4404  ssunsn2  4761  sspr  4767  sstp  4768  uniintsn  4919  brab1  5123  unopab  5157  axrep5  5216  axrep6  5217  intexab  5264  reusv2lem4  5325  reusv2  5327  el  5358  wefrc  5584  eliunxp  5749  ralxp  5753  rexxp  5754  opelco  5783  reldm0  5840  resieq  5905  iss  5946  imai  5985  cnvsym  6024  intasym  6025  asymref  6026  codir  6030  poirr2  6034  xpdifid  6076  rninxp  6087  dfpo2  6203  frpoins2fg  6251  tz6.26OLD  6255  wfis2fgOLD  6264  ordelord  6292  ordtri3  6306  dffun3OLD  6451  funopg  6475  fin  6663  f1cnvcnv  6689  funimass4  6843  fnressn  7039  resoprab  7401  mpo2eqb  7415  elrnmpores  7420  ov6g  7445  offval  7551  uniuni  7621  dfwe2  7633  orduniorsuc  7686  tfinds2  7719  dfopab2  7901  dfoprab3s  7902  fmpox  7916  fparlem1  7961  fparlem2  7962  brtpos0  8058  dftpos3  8069  tpostpos  8071  dfrecs3  8212  dfrecs3OLD  8213  tz7.48lem  8281  omeu  8425  ercnv  8528  ixp0  8728  xpcomco  8858  xpassen  8862  php  9002  phpOLD  9014  findcard3  9066  ixpfi2  9126  dfsup2  9212  sup0riota  9233  card2on  9322  infeq5i  9403  cnfcom3lem  9470  ssttrcl  9482  ttrcltr  9483  ttrclss  9487  frins2f  9520  r1elss  9573  rankxplim  9646  scott0s  9655  aceq1  9882  dfac5lem1  9888  dfac5lem2  9889  kmlem3  9917  kmlem8  9922  kmlem16  9930  djuinf  9953  cflem  10011  cf0  10016  alephval2  10337  fpwwe2lem7  10402  fpwwe2lem11  10406  rankcf  10542  r1tskina  10547  wfgru  10581  genpass  10774  psslinpr  10796  ltpsrpr  10874  addeq0  11407  infm3  11943  nnwos  12664  ioo0  13113  ico0  13134  ioc0  13135  icc0  13136  elfz2nn0  13356  elfzmlbp  13376  sqeqori  13939  hashgt12el  14146  hashgt12el2  14147  cshwidxmod  14525  clim0  15224  divalglem6  16116  ncoprmlnprm  16441  pceu  16556  prmreclem2  16627  cshwshash  16815  xpscf  17285  acsfn2  17381  invsym2  17484  cat1  17821  pospo  18072  issubmndb  18453  f1omvdco3  19066  psgnunilem5  19111  efgrelexlemb  19365  gexex  19463  srgrmhm  19781  lssne0  20221  islindf4  21054  opsrtoslem1  21271  opsrtoslem2  21272  mdetunilem8  21777  cpmatmcllem  21876  pmatcollpw2lem  21935  ntreq0  22237  ordtrest2lem  22363  ist0-3  22505  ist1-2  22507  ist1-3  22509  cmpfi  22568  2ndcctbss  22615  ptbasfi  22741  ptcnplem  22781  hausdiag  22805  hauseqlcld  22806  cnmptcom  22838  txflf  23166  tgphaus  23277  metrest  23689  iccpnfcnv  24116  bcth3  24504  dyadmax  24771  vitalilem2  24782  vitalilem3  24783  mbfimaopnlem  24828  itg2leub  24908  dvres2  25085  ellogdm  25803  reasinsin  26055  leibpilem2  26100  ftalem3  26233  dchreq  26415  legso  26969  outpasch  27125  axcontlem2  27342  incistruhgr  27458  nbgrel  27716  usgr2pth0  28142  rusgrnumwwlkslem  28343  frgr3v  28648  4cycl2vnunb  28663  frgrncvvdeqlem2  28673  lnon0  29169  spansncvi  30023  pjssmii  30052  nmlnopgt0i  30368  largei  30638  cvexchlem  30739  xfree  30815  nmo  30847  reuxfrdf  30848  fpwrelmapffslem  31076  eliccioo  31214  qtophaus  31795  ordtrest2NEWlem  31881  ordtconnlem1  31883  xrge0iifcnv  31892  xrge0iifiso  31894  xrge0iifhom  31896  cntnevol  32205  eulerpartlemgh  32354  ballotlem7  32511  signswch  32549  bnj446  32705  bnj563  32732  bnj110  32847  bnj153  32869  bnj864  32911  bnj865  32912  bnj849  32914  bnj929  32925  bnj1110  32971  fineqvac  33075  cusgr3cyclex  33107  derang0  33140  iccllysconn  33221  cvmsss2  33245  satf0op  33348  elmrsubrn  33491  quad3  33637  axacprim  33657  ralxp3f  33694  dftr6  33727  elintfv  33747  opelco3  33758  elima4  33759  setinds2f  33764  elpotr  33766  frpoins3xpg  33796  frpoins3xp3g  33797  xpord3pred  33807  wzel  33827  bdayimaon  33905  noetainflem4  33952  elfuns  34226  dfiota3  34234  brimg  34248  imagesset  34264  lineunray  34458  ellines  34463  hfninf  34497  bj-elabtru  35067  bj-snglc  35168  bj-mpomptALT  35299  bj-elid7  35351  bj-imdirco  35370  nlpineqsn  35588  curf  35764  tan2h  35778  poimirlem26  35812  poimirlem27  35813  poimirlem30  35816  poimirlem32  35818  poimir  35819  ovoliunnfl  35828  voliunnfl  35830  ftc1anc  35867  inixp  35895  heibor1lem  35976  csbcom2fi  36295  tsna1  36311  anan  36388  brid  36449  idinxpssinxp4  36462  iss2  36486  xrninxp  36525  cossssid3  36594  dmqs1cosscnvepreseq  36781  islshpat  37038  lkr0f  37115  lshpsmreu  37130  cvrnbtwn4  37300  ishlat2  37374  islvol5  37600  tendoeq2  38795  dibelval3  39168  mapdpglem3  39696  hdmapglem7a  39948  4rexfrabdioph  40627  dford4  40858  isdomn3  41036  fgraphopab  41042  ifpim123g  41114  ifpbibib  41124  rp-isfinite6  41132  elrncard  41151  undmrnresiss  41219  cnvssco  41221  iunrelexpuztr  41334  dffrege115  41593  brco2f1o  41649  ntrneiiso  41708  ismnuprim  41919  undisjrab  41931  radcnvrat  41939  opelopab4  42178  2sb5nd  42187  un2122  42417  uunT12p4  42430  2sb5ndVD  42537  2sb5ndALT  42559  ndisj2  42606  ssabf  42657  abssf  42669  fourierdlem42  43697  smflimlem4  44319  aiotaexaiotaiota  44597  ndmaovcom  44708  dmafv2rnb  44732  afv2ndeffv0  44763  0nelsetpreimafv  44853  eliunxp2  45680  pgrpgt2nabl  45713  islindeps  45805  lindslinindsimp1  45809  lindslinindsimp2  45815