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  2315  sbied  2501  sbidm  2508  mo  2558  2mosOLD  2643  2eu6  2650  cbvab  2801  nabbib  3028  rexcom4a  3259  abv  3450  ceqsex  3487  ceqsexv  3489  spc2ed  3558  clel2g  3616  2reuswap  3708  2reuswap2  3709  2reu5  3720  2rmoswap  3723  nfcdeq  3739  sbcid  3761  sbcco2  3771  sbc7  3776  sbcie2g  3785  eqsbc1  3791  sbcralt  3826  cbvralcsf  3895  cbvrabcsf  3898  abss  4017  ssab  4018  raldifb  4102  difrab  4271  euelss  4285  vn0  4298  sbccsb  4389  vdif0  4422  difrab0eq  4423  ssunsn2  4781  sspr  4789  sstp  4790  uniintsn  4938  brab1  5143  unopab  5175  axrep5  5229  axrep6OLD  5231  intexab  5288  reusv2lem4  5343  reusv2  5345  el  5384  wefrc  5617  eliunxp  5784  ralxp  5788  rexxp  5789  opelco  5818  reldm0  5874  resieq  5945  iss  5990  imai  6029  intasym  6068  asymref  6069  codir  6073  poirr2  6077  xpdifid  6121  rninxp  6132  dfpo2  6248  frpoins2fg  6296  ordelord  6333  ordtri3  6347  funopg  6520  fin  6708  f1cnvcnv  6733  funimass4  6891  fnressn  7096  resoprab  7471  mpo2eqb  7485  elrnmpores  7491  ov6g  7517  imaeqexov  7591  imaeqalov  7592  offval  7626  uniuni  7702  dfwe2  7714  orduniorsuc  7769  tfinds2  7804  dfopab2  7994  dfoprab3s  7995  fmpox  8009  fparlem1  8052  fparlem2  8053  ralxp3f  8077  frpoins3xpg  8080  brtpos0  8173  dftpos3  8184  tpostpos  8186  dfrecs3  8302  tz7.48lem  8370  omeu  8510  ercnv  8653  ixp0  8865  xpcomco  8991  xpassen  8995  php  9131  findcard3  9187  findcard3OLD  9188  ixpfi2  9259  dfsup2  9353  sup0riota  9375  card2on  9465  infeq5i  9551  cnfcom3lem  9618  ssttrcl  9630  ttrcltr  9631  ttrclss  9635  frins2f  9668  r1elss  9721  rankxplim  9794  scott0s  9803  aceq1  10030  dfac5lem1  10036  dfac5lem2  10037  kmlem3  10066  kmlem8  10071  kmlem16  10079  djuinf  10102  cflemOLD  10159  cf0  10164  alephval2  10485  fpwwe2lem7  10550  fpwwe2lem11  10554  rankcf  10690  r1tskina  10695  wfgru  10729  genpass  10922  psslinpr  10944  ltpsrpr  11022  addeq0  11561  infm3  12102  nnwos  12834  ioo0  13291  ico0  13312  ioc0  13313  icc0  13314  elfz2nn0  13539  elfzmlbp  13560  sqeqori  14139  hashgt12el  14347  hashgt12el2  14348  cshwidxmod  14727  clim0  15431  divalglem6  16327  ncoprmlnprm  16657  pceu  16776  prmreclem2  16847  cshwshash  17034  xpscf  17487  acsfn2  17587  invsym2  17688  cat1  18022  pospo  18267  issubmndb  18697  f1omvdco3  19346  psgnunilem5  19391  efgrelexlemb  19647  gexex  19750  srgrmhm  20125  isdomn3  20618  isdomn4r  20622  lssne0  20872  islindf4  21763  opsrtoslem1  21978  opsrtoslem2  21979  mdetunilem8  22522  cpmatmcllem  22621  pmatcollpw2lem  22680  ntreq0  22980  ordtrest2lem  23106  ist0-3  23248  ist1-2  23250  ist1-3  23252  cmpfi  23311  2ndcctbss  23358  ptbasfi  23484  ptcnplem  23524  hausdiag  23548  hauseqlcld  23549  cnmptcom  23581  txflf  23909  tgphaus  24020  metrest  24428  iccpnfcnv  24858  bcth3  25247  dyadmax  25515  vitalilem2  25526  vitalilem3  25527  mbfimaopnlem  25572  itg2leub  25651  dvres2  25829  ellogdm  26564  reasinsin  26822  leibpilem2  26867  ftalem3  27001  dchreq  27185  bdayimaon  27621  noetainflem4  27668  cuteq1  27766  addsprop  27906  sleadd1  27919  negsprop  27964  mulsprop  28056  mulsuniflem  28075  addsdilem1  28077  addsdilem2  28078  mulsasslem1  28089  mulsasslem2  28090  precsexlem10  28141  precsexlem11  28142  onnolt  28190  bdayn0p1  28281  legso  28562  outpasch  28718  axcontlem2  28928  incistruhgr  29042  nbgrel  29303  usgr2pth0  29728  rusgrnumwwlkslem  29932  frgr3v  30237  4cycl2vnunb  30252  frgrncvvdeqlem2  30262  lnon0  30760  spansncvi  31614  pjssmii  31643  nmlnopgt0i  31959  largei  32229  cvexchlem  32330  xfree  32406  nmo  32452  reuxfrdf  32453  fpwrelmapffslem  32688  eliccioo  32884  1arithidom  33484  ufdprmidl  33488  qtophaus  33802  ordtrest2NEWlem  33888  ordtconnlem1  33890  xrge0iifcnv  33899  xrge0iifiso  33901  xrge0iifhom  33903  cntnevol  34194  eulerpartlemgh  34345  ballotlem7  34503  signswch  34528  bnj446  34683  bnj563  34709  bnj110  34824  bnj153  34846  bnj864  34888  bnj865  34889  bnj849  34891  bnj929  34902  bnj1110  34948  fineqvac  35071  axregs  35073  cusgr3cyclex  35108  derang0  35141  iccllysconn  35222  cvmsss2  35246  satf0op  35349  elmrsubrn  35492  rexxfr3dALT  35611  quad3  35642  axacprim  35679  dftr6  35723  elintfv  35737  opelco3  35747  elima4  35748  setinds2f  35752  elpotr  35754  wzel  35797  elfuns  35888  dfiota3  35896  brimg  35910  imagesset  35926  lineunray  36120  ellines  36125  hfninf  36159  in-ax8  36197  ss-ax8  36198  bj-elabtru  36847  bj-snglc  36942  bj-mpomptALT  37092  bj-elid7  37144  bj-imdirco  37163  nlpineqsn  37381  curf  37577  tan2h  37591  poimirlem26  37625  poimirlem27  37626  poimirlem30  37629  poimirlem32  37631  poimir  37632  ovoliunnfl  37641  voliunnfl  37643  ftc1anc  37680  inixp  37707  heibor1lem  37788  csbcom2fi  38107  tsna1  38123  anan  38202  brid  38279  ref5  38286  idinxpssinxp4  38293  iss2  38311  xrninxp  38363  cossssid3  38445  dmqs1cosscnvepreseq  38639  disjxrnres5  38724  dmqsblocks  38830  islshpat  38995  lkr0f  39072  lshpsmreu  39087  cvrnbtwn4  39257  ishlat2  39331  islvol5  39558  tendoeq2  40753  dibelval3  41126  mapdpglem3  41654  hdmapglem7a  41906  4rexfrabdioph  42771  dford4  43002  fgraphopab  43176  onsupmaxb  43212  tfsconcatlem  43309  ifpim123g  43473  ifpbibib  43483  rp-isfinite6  43491  elrncard  43510  undmrnresiss  43577  cnvssco  43579  iunrelexpuztr  43692  dffrege115  43951  brco2f1o  44005  ntrneiiso  44064  ismnuprim  44267  undisjrab  44279  radcnvrat  44287  opelopab4  44525  2sb5nd  44534  un2122  44763  uunT12p4  44776  2sb5ndVD  44883  2sb5ndALT  44905  ndisj2  45029  ssabf  45078  abssf  45090  fourierdlem42  46131  smflimlem4  46756  aiotaexaiotaiota  47079  ndmaovcom  47190  dmafv2rnb  47214  afv2ndeffv0  47245  modm1p1ne  47355  0nelsetpreimafv  47375  usgrexmpl2nb0  48006  usgrexmpl2nb1  48007  gpg5nbgrvtx03starlem1  48043  gpg5nbgrvtx03starlem2  48044  gpg5nbgrvtx03starlem3  48045  gpg5nbgrvtx13starlem1  48046  gpg5nbgrvtx13starlem2  48047  gpg5nbgrvtx13starlem3  48048  pgnbgreunbgrlem2lem2  48089  eliunxp2  48306  pgrpgt2nabl  48338  islindeps  48426  lindslinindsimp1  48430  lindslinindsimp2  48436