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  1449  nanim  1498  nannot  1499  empty  1906  19.12vvv  1994  19.12vv  2349  cvjust  2730  necon1abii  2981  nrexralim  3125  r19.23v  3169  nelb  3222  cbvralsvw  3300  spc3gv  3588  ralxpxfr2d  3630  sbc8g  3778  csbied  3915  dfss2  3949  ss2rab  4051  difdif  4115  ddif  4121  unass  4152  unss  4170  undi  4265  vn0  4325  ab0orv  4363  disj  4430  ssindif0  4444  prneimg  4835  iinrab2  5051  unopab  5205  axrep5  5262  eqvinop  5467  pwssun  5550  dmun  5895  reldm0  5912  dmres  6004  imadmrn  6062  ssrnres  6172  dmsnn0  6201  coundi  6241  coundir  6242  resco  6244  cnvpo  6281  xpco  6283  dfpo2  6290  fun11  6615  fununi  6616  isarep1OLD  6632  fdmrn  6742  dffv2  6979  fsn  7130  eufnfv  7226  eloprabga  7521  funoprabg  7533  ralrnmpo  7551  imaeqexov  7650  sucexeloniOLD  7809  suceloniOLD  7811  tfinds2  7864  funcnvuni  7933  oprabrexex2  7982  ralxp3f  8141  soseq  8163  dfer2  8725  euen1b  9047  xpsnen  9074  1sdomOLD  9262  wemapsolem  9569  zfregcl  9613  epfrs  9750  rankbnd  9887  rankbnd2  9888  rankxplim2  9899  rankxplim3  9900  isinfcard  10111  dfac5lem2  10143  dfac5lem5  10146  kmlem14  10183  kmlem15  10184  kmlem16  10185  axdc2lem  10467  axcclem  10476  ac9  10502  ac9s  10512  nnunb  12502  xrrebnd  13189  elfznelfzo  13793  hashfun  14460  hashtpg  14508  rexuz3  15372  imasaddfnlem  17547  isnsgrp  18706  eqg0subg  19184  dprd2d2  20032  isnirred  20385  subsubrng2  20529  subsubrg2  20564  isdomn2OLD  20677  mdetunilem8  22562  maducoeval2  22583  tgval2  22899  0top  22926  ssntr  23001  uncmp  23346  opnfbas  23785  fbunfip  23812  alexsubALTlem2  23991  alexsubALTlem3  23992  alexsubALT  23994  metrest  24468  cfilucfil3  25277  ellimc3  25837  plyun0  26159  sinhalfpilem  26429  2lgslem4  27374  addsdilem1  28111  addsdilem2  28112  mulsasslem1  28123  mulsasslem2  28124  dfcgra2  28814  colinearalg  28894  axcontlem5  28952  nb3grprlem2  29365  wlkeq  29619  isspthonpth  29736  clwlkclwwlklem2a4  29983  clwwlkn1  30027  clwwlkn2  30030  clwwlknon2x  30089  fusgreg2wsp  30322  h2hlm  30966  shlesb1i  31372  pjneli  31709  cnlnssadj  32066  pjin2i  32179  cvnbtwn2  32273  cvnbtwn4  32275  mdsl1i  32307  mdsl2i  32308  hatomistici  32348  cdj3lem3b  32426  iuninc  32546  disjex  32578  disjexc  32579  fpwrelmapffslem  32714  fpwrelmapffs  32716  mgcval  32972  isarchi2  33188  elrgspnlem2  33243  ismntop  34062  coinfliprv  34520  ballotlem2  34526  ballotlemi1  34540  plymulx  34585  oddprm2  34692  bnj168  34766  bnj153  34916  bnj605  34943  bnj607  34952  bnj986  34991  bnj1090  35015  bnj1128  35026  fineqvrep  35131  fmlasucdisj  35426  dfso2  35777  19.12b  35824  dfom5b  35935  elfuns  35938  dfint3  35975  hfext  36206  trer  36339  bj-alcomexcom  36703  wl-3xornot1  37503  wl-df3maxtru1  37515  cnambfre  37697  itg2addnclem2  37701  itg2addnc  37703  heiborlem1  37840  inxpxrn  38418  lssat  39039  islshpat  39040  lcvnbtwn2  39050  pclfinclN  39974  lhpex2leN  40037  diclspsn  41218  dihmeetlem4preN  41330  dihmeetlem13N  41343  lcdlss  41643  mapd1o  41672  eq0rabdioph  42774  rmspecnonsq  42905  rmxdioph  43015  wopprc  43029  islssfg2  43070  ifpan23  43459  ifpid1g  43493  minregex  43533  dfrtrcl5  43628  dfhe3  43774  ntrneikb  44093  scottabf  44239  2sbc6g  44414  2sbc5g  44415  iotasbc2  44419  2sb5nd  44560  2sb5ndVD  44909  2sb5ndALT  44931  ssclaxsep  44982  permac8prim  45014  limsupre2lem  45733  2rexsb  47110  2rexrsb  47111  usgrexmpl2nb2  48017  usgrexmpl2nb5  48020  usgrexmpl2trifr  48021  islindeps  48409  io1ii  48875