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  644  anandi  673  anandir  674  orordi  926  orordir  927  ianor  979  trunantru  1581  falnanfal  1584  had0  1604  nic-axALT  1675  equsexvw  2007  sbiedvw  2095  sbievw2  2098  sbal  2158  sb6a  2248  sb56OLD  2268  sbco4  2273  sbiedw  2308  cbvsbv  2358  sbied  2501  sbidm  2508  mo  2558  2mos  2644  2eu6  2651  cbvabwOLD  2806  cbvab  2807  elisset  2814  nabbib  3044  r19.41v  3187  2ralorOLD  3228  r19.41  3259  rexcom4a  3288  abv  3484  ceqsex  3523  ceqsexv  3525  spc2ed  3591  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  5837  ralxp  5841  rexxp  5842  opelco  5871  reldm0  5927  resieq  5992  iss  6035  imai  6073  cnvsymOLDOLD  6115  intasym  6116  asymref  6117  codir  6121  poirr2  6125  xpdifid  6167  rninxp  6178  dfpo2  6295  frpoins2fg  6345  tz6.26OLD  6349  wfis2fgOLD  6358  ordelord  6386  ordtri3  6400  dffun3OLD  6558  funopg  6582  fin  6771  f1cnvcnv  6797  funimass4  6956  fnressn  7158  resoprab  7529  mpo2eqb  7544  elrnmpores  7549  ov6g  7575  imaeqexov  7649  imaeqalov  7650  offval  7683  uniuni  7753  dfwe2  7765  orduniorsuc  7822  tfinds2  7857  dfopab2  8042  dfoprab3s  8043  fmpox  8057  fparlem1  8103  fparlem2  8104  ralxp3f  8128  frpoins3xpg  8131  brtpos0  8224  dftpos3  8235  tpostpos  8237  dfrecs3  8378  dfrecs3OLD  8379  tz7.48lem  8447  omeu  8591  ercnv  8730  ixp0  8931  xpcomco  9068  xpassen  9072  php  9216  phpOLD  9228  findcard3  9291  findcard3OLD  9292  ixpfi2  9356  dfsup2  9445  sup0riota  9466  card2on  9555  infeq5i  9637  cnfcom3lem  9704  ssttrcl  9716  ttrcltr  9717  ttrclss  9721  frins2f  9754  r1elss  9807  rankxplim  9880  scott0s  9889  aceq1  10118  dfac5lem1  10124  dfac5lem2  10125  kmlem3  10153  kmlem8  10158  kmlem16  10166  djuinf  10189  cflem  10247  cf0  10252  alephval2  10573  fpwwe2lem7  10638  fpwwe2lem11  10642  rankcf  10778  r1tskina  10783  wfgru  10817  genpass  11010  psslinpr  11032  ltpsrpr  11110  addeq0  11644  infm3  12180  nnwos  12906  ioo0  13356  ico0  13377  ioc0  13378  icc0  13379  elfz2nn0  13599  elfzmlbp  13619  sqeqori  14185  hashgt12el  14389  hashgt12el2  14390  cshwidxmod  14760  clim0  15457  divalglem6  16348  ncoprmlnprm  16671  pceu  16786  prmreclem2  16857  cshwshash  17045  xpscf  17518  acsfn2  17614  invsym2  17717  cat1  18057  pospo  18308  issubmndb  18728  f1omvdco3  19365  psgnunilem5  19410  efgrelexlemb  19666  gexex  19769  srgrmhm  20123  lssne0  20794  islindf4  21703  opsrtoslem1  21927  opsrtoslem2  21928  mdetunilem8  22441  cpmatmcllem  22540  pmatcollpw2lem  22599  ntreq0  22901  ordtrest2lem  23027  ist0-3  23169  ist1-2  23171  ist1-3  23173  cmpfi  23232  2ndcctbss  23279  ptbasfi  23405  ptcnplem  23445  hausdiag  23469  hauseqlcld  23470  cnmptcom  23502  txflf  23830  tgphaus  23941  metrest  24353  iccpnfcnv  24789  bcth3  25179  dyadmax  25447  vitalilem2  25458  vitalilem3  25459  mbfimaopnlem  25504  itg2leub  25584  dvres2  25761  ellogdm  26487  reasinsin  26742  leibpilem2  26787  ftalem3  26920  dchreq  27104  bdayimaon  27539  noetainflem4  27586  cuteq1  27679  addsprop  27806  sleadd1  27819  negsprop  27860  mulsprop  27943  mulsuniflem  27962  addsdilem1  27964  addsdilem2  27965  mulsasslem1  27976  mulsasslem2  27977  precsexlem10  28027  precsexlem11  28028  legso  28283  outpasch  28439  axcontlem2  28656  incistruhgr  28772  nbgrel  29030  usgr2pth0  29455  rusgrnumwwlkslem  29656  frgr3v  29961  4cycl2vnunb  29976  frgrncvvdeqlem2  29986  lnon0  30484  spansncvi  31338  pjssmii  31367  nmlnopgt0i  31683  largei  31953  cvexchlem  32054  xfree  32130  nmo  32163  reuxfrdf  32164  fpwrelmapffslem  32390  eliccioo  32530  qtophaus  33280  ordtrest2NEWlem  33366  ordtconnlem1  33368  xrge0iifcnv  33377  xrge0iifiso  33379  xrge0iifhom  33381  cntnevol  33690  eulerpartlemgh  33841  ballotlem7  33998  signswch  34036  bnj446  34192  bnj563  34218  bnj110  34333  bnj153  34355  bnj864  34397  bnj865  34398  bnj849  34400  bnj929  34411  bnj1110  34457  fineqvac  34561  cusgr3cyclex  34591  derang0  34624  iccllysconn  34705  cvmsss2  34729  satf0op  34832  elmrsubrn  34975  quad3  35119  axacprim  35146  dftr6  35191  elintfv  35206  opelco3  35216  elima4  35217  setinds2f  35221  elpotr  35223  wzel  35266  elfuns  35357  dfiota3  35365  brimg  35379  imagesset  35395  lineunray  35589  ellines  35594  hfninf  35628  bj-elabtru  36217  bj-snglc  36314  bj-mpomptALT  36464  bj-elid7  36516  bj-imdirco  36535  nlpineqsn  36753  curf  36930  tan2h  36944  poimirlem26  36978  poimirlem27  36979  poimirlem30  36982  poimirlem32  36984  poimir  36985  ovoliunnfl  36994  voliunnfl  36996  ftc1anc  37033  inixp  37060  heibor1lem  37141  csbcom2fi  37460  tsna1  37476  anan  37557  brid  37639  ref5  37646  idinxpssinxp4  37653  iss2  37677  xrninxp  37726  cossssid3  37803  dmqs1cosscnvepreseq  37996  disjxrnres5  38081  islshpat  38351  lkr0f  38428  lshpsmreu  38443  cvrnbtwn4  38613  ishlat2  38687  islvol5  38914  tendoeq2  40109  dibelval3  40482  mapdpglem3  41010  hdmapglem7a  41262  4rexfrabdioph  41999  dford4  42231  isdomn3  42409  fgraphopab  42415  onsupmaxb  42451  tfsconcatlem  42549  ifpim123g  42714  ifpbibib  42724  rp-isfinite6  42732  elrncard  42751  undmrnresiss  42818  cnvssco  42820  iunrelexpuztr  42933  dffrege115  43192  brco2f1o  43246  ntrneiiso  43305  ismnuprim  43516  undisjrab  43528  radcnvrat  43536  opelopab4  43775  2sb5nd  43784  un2122  44014  uunT12p4  44027  2sb5ndVD  44134  2sb5ndALT  44156  ndisj2  44200  ssabf  44251  abssf  44263  fourierdlem42  45324  smflimlem4  45949  aiotaexaiotaiota  46261  ndmaovcom  46372  dmafv2rnb  46396  afv2ndeffv0  46427  0nelsetpreimafv  46517  eliunxp2  47172  pgrpgt2nabl  47205  islindeps  47296  lindslinindsimp1  47300  lindslinindsimp2  47306