Theorem bitr2i 276

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 12-Mar-1993.)

Hypotheses

Ref	Expression
bitr2i.1	⊢ (𝜑 ↔ 𝜓)
bitr2i.2	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
bitr2i	⊢ (𝜒 ↔ 𝜑)

Proof of Theorem bitr2i

Step	Hyp	Ref	Expression
1		bitr2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		bitr2i.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3	1, 2	bitri 275	. 2 ⊢ (𝜑 ↔ 𝜒)
4	3	bicomi 224	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  3bitr2ri  300  3bitr4ri  304  nan  829  pm4.15  832  pm5.7  955  pm5.17  1013  pm4.83  1026  3or6  1448  nanim  1497  nannot  1498  empty  1905  19.12vvv  1987  19.12vv  2348  cvjust  2730  necon1abii  2988  nrexralim  3136  r19.23v  3182  nelb  3233  cbvralsvw  3316  spc3gv  3603  ralxpxfr2d  3645  sbc8g  3795  csbied  3934  dfss2  3968  ss2rab  4070  difdif  4134  ddif  4140  unass  4171  unss  4189  undi  4284  vn0  4344  ab0orv  4382  disj  4449  ssindif0  4463  prneimg  4853  iinrab2  5069  unopab  5223  axrep5  5286  eqvinop  5491  pwssun  5574  dmun  5920  reldm0  5937  dmres  6029  imadmrn  6087  ssrnres  6197  dmsnn0  6226  coundi  6266  coundir  6267  resco  6269  cnvpo  6306  xpco  6308  dfpo2  6315  fun11  6639  fununi  6640  isarep1OLD  6656  fdmrn  6766  dffv2  7003  fsn  7154  eufnfv  7250  eloprabga  7543  funoprabg  7555  ralrnmpo  7573  imaeqexov  7672  sucexeloniOLD  7831  suceloniOLD  7833  tfinds2  7886  funcnvuni  7955  oprabrexex2  8004  ralxp3f  8163  soseq  8185  dfer2  8747  euen1b  9069  xpsnen  9096  1sdomOLD  9286  wemapsolem  9591  zfregcl  9635  epfrs  9772  rankbnd  9909  rankbnd2  9910  rankxplim2  9921  rankxplim3  9922  isinfcard  10133  dfac5lem2  10165  dfac5lem5  10168  kmlem14  10205  kmlem15  10206  kmlem16  10207  axdc2lem  10489  axcclem  10498  ac9  10524  ac9s  10534  nnunb  12524  xrrebnd  13211  elfznelfzo  13812  hashfun  14477  hashtpg  14525  rexuz3  15388  imasaddfnlem  17574  isnsgrp  18737  eqg0subg  19215  dprd2d2  20065  isnirred  20421  subsubrng2  20565  subsubrg2  20600  isdomn2OLD  20713  mdetunilem8  22626  maducoeval2  22647  tgval2  22964  0top  22991  ssntr  23067  uncmp  23412  opnfbas  23851  fbunfip  23878  alexsubALTlem2  24057  alexsubALTlem3  24058  alexsubALT  24060  metrest  24538  cfilucfil3  25355  ellimc3  25915  plyun0  26237  sinhalfpilem  26506  2lgslem4  27451  addsdilem1  28178  addsdilem2  28179  mulsasslem1  28190  mulsasslem2  28191  dfcgra2  28839  colinearalg  28926  axcontlem5  28984  nb3grprlem2  29399  wlkeq  29653  isspthonpth  29770  clwlkclwwlklem2a4  30017  clwwlkn1  30061  clwwlkn2  30064  clwwlknon2x  30123  fusgreg2wsp  30356  h2hlm  31000  shlesb1i  31406  pjneli  31743  cnlnssadj  32100  pjin2i  32213  cvnbtwn2  32307  cvnbtwn4  32309  mdsl1i  32341  mdsl2i  32342  hatomistici  32382  cdj3lem3b  32460  iuninc  32574  disjex  32606  disjexc  32607  fpwrelmapffslem  32744  fpwrelmapffs  32746  mgcval  32978  isarchi2  33193  elrgspnlem2  33248  ismntop  34028  coinfliprv  34486  ballotlem2  34492  ballotlemi1  34506  plymulx  34564  oddprm2  34671  bnj168  34745  bnj153  34895  bnj605  34922  bnj607  34931  bnj986  34970  bnj1090  34994  bnj1128  35005  fineqvrep  35110  fmlasucdisj  35405  dfso2  35756  19.12b  35803  dfom5b  35914  elfuns  35917  dfint3  35954  hfext  36185  trer  36318  bj-alcomexcom  36682  wl-3xornot1  37482  wl-df3maxtru1  37494  cnambfre  37676  itg2addnclem2  37680  itg2addnc  37682  heiborlem1  37819  inxpxrn  38397  lssat  39018  islshpat  39019  lcvnbtwn2  39029  pclfinclN  39953  lhpex2leN  40016  diclspsn  41197  dihmeetlem4preN  41309  dihmeetlem13N  41322  lcdlss  41622  mapd1o  41651  eq0rabdioph  42792  rmspecnonsq  42923  rmxdioph  43033  wopprc  43047  islssfg2  43088  ifpan23  43478  ifpid1g  43512  minregex  43552  dfrtrcl5  43647  dfhe3  43793  ntrneikb  44112  scottabf  44264  2sbc6g  44439  2sbc5g  44440  iotasbc2  44444  2sb5nd  44585  2sb5ndVD  44935  2sb5ndALT  44957  ssclaxsep  45004  limsupre2lem  45744  2rexsb  47118  2rexrsb  47119  usgrexmpl2nb2  47997  usgrexmpl2nb5  48000  usgrexmpl2trifr  48001  islindeps  48375  io1ii  48825