Theorem bitr3i 280

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitrri  301  3bitr3i  304  3bitr3ri  305  xchnxbi  335  an13  660  anandi  689  anandir  690  orordi  942  orordir  943  ianor  997  trunantru  1611  falnanfal  1614  had0OLD  1636  nic-axALT  1707  equsexvw  2038  sbiedvw  2132  sbievw2  2135  cbvsbv  2137  sbal  2206  sb6a  2292  sbiedw  2346  sbied  2532  sbidm  2539  mo  2590  2eu6  2681  cbvab  2832  nabbib  3060  rexcom4a  3292  abv  3462  ceqsex  3497  ceqsexv  3498  spc2ed  3555  clel2g  3612  2reuswap  3703  2reuswap2  3704  2reu5  3715  2rmoswap  3718  nfcdeq  3734  sbcid  3755  sbcco2  3765  sbc7  3770  sbcie2g  3778  eqsbc1  3784  sbcralt  3818  cbvralcsf  3888  cbvrabcsf  3891  abss  4009  ssab  4010  raldifb  4095  difrab  4263  euelss  4277  sbccsb  4393  vdif0  4421  difrab0eq  4422  ssunsn2  4787  sspr  4794  sstp  4795  uniintsn  4944  brab1  5152  unopab  5184  axrep5  5238  intexab  5306  reusv2lem4  5362  reusv2  5364  el.OLD  5406  wefrc  5641  eliunxp  5810  ralxp  5814  rexxp  5815  opelco  5845  reldm0  5906  resieq  5977  iss  6025  imai  6064  intasym  6103  asymref  6104  codir  6108  poirr2  6112  xpdifid  6154  rninxp  6166  dfpo2  6288  frpoins2fg  6336  ordelord  6373  ordtri3  6388  funopg  6562  fin  6750  f1cnvcnv  6777  funimass4  6937  fnressn  7150  resoprab  7526  mpo2eqb  7540  elrnmpores  7546  ov6g  7572  imaeqexov  7647  imaeqalov  7648  mpt3mpt  7673  offval  7685  uniuni  7759  dfwe2  7771  orduniorsuc  7824  tfinds2  7858  dfopab2  8046  dfoprab3s  8047  fmpox  8061  fparlem1  8106  fparlem2  8107  ralxp3f  8132  frpoins3xpg  8135  brtpos0  8228  dftpos3  8239  tpostpos  8241  dfrecs3  8358  tz7.48lemOLD  8429  omeu  8571  ercnv  8717  curf  8868  ixp0  8937  xpcomco  9064  xpassen  9068  php  9200  findcard3  9252  ixpfi2  9317  dfsup2  9414  sup0riota  9436  card2on  9526  infeq5i  9615  cnfcom3lem  9682  ssttrcl  9694  ttrcltr  9695  ttrclss  9699  setinds2f  9729  frins2f  9735  r1elss  9788  rankxplim  9869  scott0bs  9916  scott0bsOLD  9917  aceq1  10168  dfac5lem1  10174  dfac5lem2  10175  kmlem3  10203  kmlem8  10208  kmlem16  10216  djuinf  10239  cf0  10300  alephval2  10629  fpwwe2lem7  10694  fpwwe2lem11  10698  rankcf  10834  r1tskina  10839  wfgru  10873  genpass  11066  psslinpr  11088  ltpsrpr  11166  addeq0  11709  infm3  12246  nnwos  13012  ioo0  13471  ico0  13492  ioc0  13493  icc0  13494  elfz2nn0  13721  elfzmlbp  13742  sqeqori  14326  hashgt12el  14535  hashgt12el2  14536  cshwidxmod  14922  clim0  15641  divalglem6  16536  ncoprmlnprm  16867  pceu  16986  prmreclem2  17057  cshwshash  17244  xpscf  17699  acsfn2  17799  invsym2  17900  cat1  18234  pospo  18479  issubmndb  18962  f1omvdco3  19625  psgnunilem5  19670  efgrelexlemb  19926  gexex  20029  srgrmhm  20410  dfring3  20480  isdomn3  20928  isdomn4r  20932  lssne0  21188  islindf4  22106  opsrtoslem1  22326  opsrtoslem2  22327  mdetunilem8  22896  cpmatmcllem  22998  pmatcollpw2lem  23057  ntreq0  23357  ordtrest2lem  23483  ist0-3  23625  ist1-2  23627  ist1-3  23629  cmpfi  23688  2ndcctbss  23736  ptbasfi  23862  ptcnplem  23902  hausdiag  23926  hauseqlcld  23927  cnmptcom  23959  txflf  24287  tgphaus  24398  metrest  24805  iccpnfcnv  25227  bcth3  25614  dyadmax  25881  vitalilem2  25892  vitalilem3  25893  mbfimaopnlem  25938  itg2leub  26017  dvres2  26194  ellogdm  26931  reasinsin  27188  leibpilem2  27233  ftalem3  27366  dchreq  27549  bdayimaon  27984  noetainflem4  28031  cuteq1  28137  addsprop  28296  leadds1  28309  negsprop  28355  mulsprop  28450  mulsuniflem  28469  addsdilem1  28471  addsdilem2  28472  mulsasslem1  28483  mulsasslem2  28484  precsexlem10  28536  precsexlem11  28537  onnolt  28586  bdayn0p1  28689  legso  28996  outpasch  29167  axcontlem2  29477  incistruhgr  29591  nbgrel  29855  usgr2pth0  30285  rusgrnumwwlkslem  30495  frgr3v  30810  4cycl2vnunb  30825  frgrncvvdeqlem2  30835  lnon0  31334  spansncvi  32188  pjssmii  32217  nmlnopgt0i  32533  largei  32803  cvexchlem  32904  xfree  32980  nmo  33020  reuxfrdf  33021  fpwrelmapffslem  33258  eliccioo  33431  1arithidom  34003  ufdprmidl  34007  qtophaus  34402  ordtrest2NEWlem  34488  ordtconnlem1  34490  xrge0iifcnv  34499  xrge0iifiso  34501  xrge0iifhom  34503  cntnevol  34795  eulerpartlemgh  34945  ballotlem7  35103  signswch  35125  bnj446  35283  bnj563  35309  bnj110  35423  bnj153  35445  bnj864  35487  bnj865  35488  bnj849  35490  bnj929  35501  bnj1110  35547  onrankid  35658  fineqvac  35709  axregs  35732  cusgr3cyclex  35832  derang0  35855  iccllysconn  35936  cvmsss2  35960  satf0op  36063  elmrsubrn  36206  rexxfr3dALT  36325  quad3  36356  axacprim  36393  dftr6  36437  elintfv  36451  opelco3  36461  elima4  36462  elpotr  36465  wzel  36508  elfuns  36599  dfiota3  36607  brimg  36621  imagesset  36639  lineunray  36834  ellines  36839  hfninf  36857  in-ax8  36935  ss-ax8  36936  bj-df-sb  37471  bj-elabtru  37708  bj-snglc  37804  bj-mpomptALT  37960  bj-elid7  38012  bj-imdirco  38031  nlpineqsn  38251  tan2h  38455  poimirlem26  38484  poimirlem27  38485  poimirlem30  38488  poimirlem32  38490  poimir  38491  ovoliunnfl  38500  voliunnfl  38502  ftc1anc  38539  inixp  38582  heibor1lem  38663  csbcom2fi  38980  tsna1  38996  anan  39087  brid  39164  ref5  39171  idinxpssinxp4  39178  iss2  39196  raldmqseu  39217  xrninxp  39267  cossssid3  39411  dmqs1cosscnvepreseq  39599  disjxrnres5  39699  dmqsblocks  39819  islshpat  39994  lkr0f  40071  lshpsmreu  40086  cvrnbtwn4  40256  ishlat2  40330  islvol5  40556  tendoeq2  41751  dibelval3  42124  mapdpglem3  42652  hdmapglem7a  42904  4rexfrabdioph  43743  dford4  43974  fgraphopab  44148  onsupmaxb  44184  tfsconcatlem  44281  ifpim123g  44444  ifpbibib  44454  rp-isfinite6  44462  elrncard  44481  undmrnresiss  44548  cnvssco  44550  iunrelexpuztr  44663  dffrege115  44922  brco2f1o  44976  ntrneiiso  45035  ismnuprim  45222  undisjrab  45234  radcnvrat  45242  opelopab4  45478  2sb5nd  45487  un2122  45716  uunT12p4  45729  2sb5ndVD  45836  2sb5ndALT  45858  ndisj2  45989  ssabf  46036  abssf  46048  fourierdlem42  47081  smflimlem4  47706  aiotaexaiotaiota  48086  ndmaovcom  48197  dmafv2rnb  48221  afv2ndeffv0  48252  modm1p1ne  48368  0nelsetpreimafv  48394  usgrexmpl2nb0  49051  usgrexmpl2nb1  49052  gpg5nbgrvtx03starlem1  49088  gpg5nbgrvtx03starlem2  49089  gpg5nbgrvtx03starlem3  49090  gpg5nbgrvtx13starlem1  49091  gpg5nbgrvtx13starlem2  49092  gpg5nbgrvtx13starlem3  49093  pgnbgreunbgrlem2lem2  49135  gpg5edgnedg  49150  eliunxp2  49368  pgrpgt2nabl  49400  islindeps  49487  lindslinindsimp1  49491  lindslinindsimp2  49497