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  1581  falnanfal  1584  had0  1604  nic-axALT  1674  equsexvw  2005  sbiedvw  2096  sbievw2  2099  cbvsbv  2101  sbal  2170  sbco4OLD  2176  sb6a  2259  sbiedw  2317  sbied  2508  sbidm  2515  mo  2565  2mosOLD  2650  2eu6  2657  cbvab  2808  nabbib  3036  2ralorOLD  3220  rexcom4a  3277  abv  3476  ceqsex  3514  ceqsexv  3516  spc2ed  3585  clel2g  3643  2reuswap  3734  2reuswap2  3735  2reu5  3746  2rmoswap  3749  nfcdeq  3765  sbcid  3787  sbcco2  3797  sbc7  3802  sbcie2g  3811  eqsbc1  3817  sbcralt  3852  cbvralcsf  3921  cbvrabcsf  3924  abss  4043  ssab  4044  raldifb  4129  difrab  4298  euelss  4312  vn0  4325  sbccsb  4416  vdif0  4449  difrab0eq  4450  ssunsn2  4808  sspr  4816  sstp  4817  uniintsn  4966  brab1  5172  unopab  5205  axrep5  5262  axrep6OLD  5264  intexab  5321  reusv2lem4  5376  reusv2  5378  el  5417  wefrc  5653  eliunxp  5822  ralxp  5826  rexxp  5827  opelco  5856  reldm0  5912  resieq  5982  iss  6027  imai  6066  cnvsymOLDOLD  6108  intasym  6109  asymref  6110  codir  6114  poirr2  6118  xpdifid  6162  rninxp  6173  dfpo2  6290  frpoins2fg  6338  tz6.26OLD  6342  wfis2fgOLD  6351  ordelord  6379  ordtri3  6393  dffun3OLD  6551  funopg  6575  fin  6763  f1cnvcnv  6788  funimass4  6948  fnressn  7153  resoprab  7530  mpo2eqb  7544  elrnmpores  7550  ov6g  7576  imaeqexov  7650  imaeqalov  7651  offval  7685  uniuni  7761  dfwe2  7773  orduniorsuc  7829  tfinds2  7864  dfopab2  8056  dfoprab3s  8057  fmpox  8071  fparlem1  8116  fparlem2  8117  ralxp3f  8141  frpoins3xpg  8144  brtpos0  8237  dftpos3  8248  tpostpos  8250  dfrecs3  8391  dfrecs3OLD  8392  tz7.48lem  8460  omeu  8602  ercnv  8745  ixp0  8950  xpcomco  9081  xpassen  9085  php  9226  phpOLD  9236  findcard3  9295  findcard3OLD  9296  ixpfi2  9367  dfsup2  9461  sup0riota  9483  card2on  9573  infeq5i  9655  cnfcom3lem  9722  ssttrcl  9734  ttrcltr  9735  ttrclss  9739  frins2f  9772  r1elss  9825  rankxplim  9898  scott0s  9907  aceq1  10136  dfac5lem1  10142  dfac5lem2  10143  kmlem3  10172  kmlem8  10177  kmlem16  10185  djuinf  10208  cflemOLD  10265  cf0  10270  alephval2  10591  fpwwe2lem7  10656  fpwwe2lem11  10660  rankcf  10796  r1tskina  10801  wfgru  10835  genpass  11028  psslinpr  11050  ltpsrpr  11128  addeq0  11665  infm3  12206  nnwos  12936  ioo0  13392  ico0  13413  ioc0  13414  icc0  13415  elfz2nn0  13640  elfzmlbp  13661  sqeqori  14237  hashgt12el  14445  hashgt12el2  14446  cshwidxmod  14826  clim0  15527  divalglem6  16422  ncoprmlnprm  16752  pceu  16871  prmreclem2  16942  cshwshash  17129  xpscf  17584  acsfn2  17680  invsym2  17781  cat1  18115  pospo  18360  issubmndb  18788  f1omvdco3  19435  psgnunilem5  19480  efgrelexlemb  19736  gexex  19839  srgrmhm  20187  isdomn3  20680  isdomn4r  20684  lssne0  20913  islindf4  21803  opsrtoslem1  22018  opsrtoslem2  22019  mdetunilem8  22562  cpmatmcllem  22661  pmatcollpw2lem  22720  ntreq0  23020  ordtrest2lem  23146  ist0-3  23288  ist1-2  23290  ist1-3  23292  cmpfi  23351  2ndcctbss  23398  ptbasfi  23524  ptcnplem  23564  hausdiag  23588  hauseqlcld  23589  cnmptcom  23621  txflf  23949  tgphaus  24060  metrest  24468  iccpnfcnv  24898  bcth3  25288  dyadmax  25556  vitalilem2  25567  vitalilem3  25568  mbfimaopnlem  25613  itg2leub  25692  dvres2  25870  ellogdm  26605  reasinsin  26863  leibpilem2  26908  ftalem3  27042  dchreq  27226  bdayimaon  27662  noetainflem4  27709  cuteq1  27803  addsprop  27940  sleadd1  27953  negsprop  27998  mulsprop  28090  mulsuniflem  28109  addsdilem1  28111  addsdilem2  28112  mulsasslem1  28123  mulsasslem2  28124  precsexlem10  28175  precsexlem11  28176  onnolt  28224  bdayn0p1  28315  legso  28583  outpasch  28739  axcontlem2  28949  incistruhgr  29063  nbgrel  29324  usgr2pth0  29752  rusgrnumwwlkslem  29956  frgr3v  30261  4cycl2vnunb  30276  frgrncvvdeqlem2  30286  lnon0  30784  spansncvi  31638  pjssmii  31667  nmlnopgt0i  31983  largei  32253  cvexchlem  32354  xfree  32430  nmo  32476  reuxfrdf  32477  fpwrelmapffslem  32714  eliccioo  32910  1arithidom  33557  ufdprmidl  33561  qtophaus  33872  ordtrest2NEWlem  33958  ordtconnlem1  33960  xrge0iifcnv  33969  xrge0iifiso  33971  xrge0iifhom  33973  cntnevol  34264  eulerpartlemgh  34415  ballotlem7  34573  signswch  34598  bnj446  34753  bnj563  34779  bnj110  34894  bnj153  34916  bnj864  34958  bnj865  34959  bnj849  34961  bnj929  34972  bnj1110  35018  fineqvac  35133  cusgr3cyclex  35163  derang0  35196  iccllysconn  35277  cvmsss2  35301  satf0op  35404  elmrsubrn  35547  rexxfr3dALT  35666  quad3  35697  axacprim  35729  dftr6  35773  elintfv  35787  opelco3  35797  elima4  35798  setinds2f  35802  elpotr  35804  wzel  35847  elfuns  35938  dfiota3  35946  brimg  35960  imagesset  35976  lineunray  36170  ellines  36175  hfninf  36209  in-ax8  36247  ss-ax8  36248  bj-elabtru  36897  bj-snglc  36992  bj-mpomptALT  37142  bj-elid7  37194  bj-imdirco  37213  nlpineqsn  37431  curf  37627  tan2h  37641  poimirlem26  37675  poimirlem27  37676  poimirlem30  37679  poimirlem32  37681  poimir  37682  ovoliunnfl  37691  voliunnfl  37693  ftc1anc  37730  inixp  37757  heibor1lem  37838  csbcom2fi  38157  tsna1  38173  anan  38252  brid  38329  ref5  38336  idinxpssinxp4  38343  iss2  38367  xrninxp  38415  cossssid3  38492  dmqs1cosscnvepreseq  38685  disjxrnres5  38770  islshpat  39040  lkr0f  39117  lshpsmreu  39132  cvrnbtwn4  39302  ishlat2  39376  islvol5  39603  tendoeq2  40798  dibelval3  41171  mapdpglem3  41699  hdmapglem7a  41951  4rexfrabdioph  42796  dford4  43028  fgraphopab  43202  onsupmaxb  43238  tfsconcatlem  43335  ifpim123g  43499  ifpbibib  43509  rp-isfinite6  43517  elrncard  43536  undmrnresiss  43603  cnvssco  43605  iunrelexpuztr  43718  dffrege115  43977  brco2f1o  44031  ntrneiiso  44090  ismnuprim  44293  undisjrab  44305  radcnvrat  44313  opelopab4  44551  2sb5nd  44560  un2122  44789  uunT12p4  44802  2sb5ndVD  44909  2sb5ndALT  44931  ndisj2  45055  ssabf  45104  abssf  45116  fourierdlem42  46158  smflimlem4  46783  aiotaexaiotaiota  47103  ndmaovcom  47214  dmafv2rnb  47238  afv2ndeffv0  47269  0nelsetpreimafv  47384  usgrexmpl2nb0  48015  usgrexmpl2nb1  48016  gpg5nbgrvtx03starlem1  48050  gpg5nbgrvtx03starlem2  48051  gpg5nbgrvtx03starlem3  48052  gpg5nbgrvtx13starlem1  48053  gpg5nbgrvtx13starlem2  48054  gpg5nbgrvtx13starlem3  48055  eliunxp2  48289  pgrpgt2nabl  48321  islindeps  48409  lindslinindsimp1  48413  lindslinindsimp2  48419