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  830  pm4.15  833  pm5.7  956  pm5.17  1014  pm4.83  1027  3or6  1450  nanim  1500  nannot  1501  empty  1908  19.12vvv  1996  19.12vv  2352  cvjust  2731  necon1abii  2981  nrexralim  3122  r19.23v  3165  nelb  3214  cbvralsvw  3289  spc3gv  3547  ralxpxfr2d  3589  sbc8g  3737  csbied  3874  dfss2  3908  ss2rab  4010  difdif  4076  ddif  4082  unass  4113  unss  4131  undi  4226  disj  4391  ssindif0  4405  prneimg  4798  iinrab2  5013  unopab  5166  axrep5  5220  eqvinop  5433  pwssun  5514  dmun  5857  reldm0  5875  dmres  5969  imadmrn  6027  ssrnres  6134  dmsnn0  6163  coundi  6203  coundir  6204  resco  6206  cnvpo  6243  xpco  6245  dfpo2  6252  fun11  6564  fununi  6565  fdmrn  6691  dffv2  6927  fsn  7080  eufnfv  7175  eloprabga  7467  funoprabg  7479  ralrnmpo  7497  imaeqexov  7596  tfinds2  7806  funcnvuni  7874  oprabrexex2  7922  ralxp3f  8078  soseq  8100  dfer2  8635  euen1b  8966  xpsnen  8990  wemapsolem  9456  zfregcl  9500  zfregclOLD  9501  epfrs  9641  rankbnd  9781  rankbnd2  9782  rankxplim2  9793  rankxplim3  9794  isinfcard  10003  dfac5lem2  10035  dfac5lem5  10038  kmlem14  10075  kmlem15  10076  kmlem16  10077  axdc2lem  10359  axcclem  10368  ac9  10394  ac9s  10404  nnunb  12422  xrrebnd  13109  elfznelfzo  13717  hashfun  14388  hashtpg  14436  rexuz3  15300  imasaddfnlem  17481  isnsgrp  18680  eqg0subg  19160  dprd2d2  20010  isnirred  20389  subsubrng2  20530  subsubrg2  20565  isdomn2OLD  20678  mdetunilem8  22593  maducoeval2  22614  tgval2  22930  0top  22957  ssntr  23032  uncmp  23377  opnfbas  23816  fbunfip  23843  alexsubALTlem2  24022  alexsubALTlem3  24023  alexsubALT  24025  metrest  24498  cfilucfil3  25296  ellimc3  25855  plyun0  26174  sinhalfpilem  26443  2lgslem4  27388  addsdilem1  28162  addsdilem2  28163  mulsasslem1  28174  mulsasslem2  28175  dfcgra2  28917  colinearalg  28998  axcontlem5  29056  nb3grprlem2  29469  wlkeq  29722  isspthonpth  29837  clwlkclwwlklem2a4  30087  clwwlkn1  30131  clwwlkn2  30134  clwwlknon2x  30193  fusgreg2wsp  30426  h2hlm  31071  shlesb1i  31477  pjneli  31814  cnlnssadj  32171  pjin2i  32284  cvnbtwn2  32378  cvnbtwn4  32380  mdsl1i  32412  mdsl2i  32413  hatomistici  32453  cdj3lem3b  32531  iuninc  32650  disjex  32682  disjexc  32683  fpwrelmapffslem  32825  fpwrelmapffs  32827  mgcval  33067  isarchi2  33266  elrgspnlem2  33324  ismntop  34191  coinfliprv  34648  ballotlem2  34654  ballotlemi1  34668  plymulx  34713  oddprm2  34820  bnj168  34894  bnj153  35043  bnj605  35070  bnj607  35079  bnj986  35118  bnj1090  35142  bnj1128  35153  fineqvrep  35279  axregszf  35294  axregs  35304  fmlasucdisj  35602  dfso2  35958  19.12b  36002  dfom5b  36113  elfuns  36116  dfint3  36155  hfext  36386  trer  36519  bj-alcomexcom  36988  wl-3xornot1  37807  wl-df3maxtru1  37819  cnambfre  38000  itg2addnclem2  38004  itg2addnc  38006  heiborlem1  38143  inxpxrn  38750  eldisjdmqsim  39149  lssat  39473  islshpat  39474  lcvnbtwn2  39484  pclfinclN  40407  lhpex2leN  40470  diclspsn  41651  dihmeetlem4preN  41763  dihmeetlem13N  41776  lcdlss  42076  mapd1o  42105  eq0rabdioph  43219  rmspecnonsq  43350  rmxdioph  43459  wopprc  43473  islssfg2  43514  ifpan23  43902  ifpid1g  43936  minregex  43976  dfrtrcl5  44071  dfhe3  44217  ntrneikb  44536  scottabf  44682  2sbc6g  44857  2sbc5g  44858  iotasbc2  44862  2sb5nd  45002  2sb5ndVD  45351  2sb5ndALT  45373  ssclaxsep  45424  permac8prim  45456  limsupre2lem  46167  2rexsb  47546  2rexrsb  47547  usgrexmpl2nb2  48506  usgrexmpl2nb5  48509  usgrexmpl2trifr  48510  islindeps  48926  io1ii  49393