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  3121  r19.23v  3164  nelb  3213  cbvralsvw  3288  spc3gv  3559  ralxpxfr2d  3601  sbc8g  3749  csbied  3886  dfss2  3920  ss2rab  4022  difdif  4088  ddif  4094  unass  4125  unss  4143  undi  4238  disj  4403  ssindif0  4417  prneimg  4811  iinrab2  5026  unopab  5179  axrep5  5233  eqvinop  5436  pwssun  5517  dmun  5860  reldm0  5878  dmres  5972  imadmrn  6030  ssrnres  6137  dmsnn0  6166  coundi  6206  coundir  6207  resco  6209  cnvpo  6246  xpco  6248  dfpo2  6255  fun11  6567  fununi  6568  fdmrn  6694  dffv2  6930  fsn  7082  eufnfv  7177  eloprabga  7469  funoprabg  7481  ralrnmpo  7499  imaeqexov  7598  tfinds2  7808  funcnvuni  7876  oprabrexex2  7924  ralxp3f  8081  soseq  8103  dfer2  8638  euen1b  8969  xpsnen  8993  wemapsolem  9459  zfregcl  9503  zfregclOLD  9504  epfrs  9644  rankbnd  9784  rankbnd2  9785  rankxplim2  9796  rankxplim3  9797  isinfcard  10006  dfac5lem2  10038  dfac5lem5  10041  kmlem14  10078  kmlem15  10079  kmlem16  10080  axdc2lem  10362  axcclem  10371  ac9  10397  ac9s  10407  nnunb  12401  xrrebnd  13087  elfznelfzo  13693  hashfun  14364  hashtpg  14412  rexuz3  15276  imasaddfnlem  17453  isnsgrp  18652  eqg0subg  19129  dprd2d2  19979  isnirred  20360  subsubrng2  20501  subsubrg2  20536  isdomn2OLD  20649  mdetunilem8  22567  maducoeval2  22588  tgval2  22904  0top  22931  ssntr  23006  uncmp  23351  opnfbas  23790  fbunfip  23817  alexsubALTlem2  23996  alexsubALTlem3  23997  alexsubALT  23999  metrest  24472  cfilucfil3  25280  ellimc3  25840  plyun0  26162  sinhalfpilem  26432  2lgslem4  27377  addsdilem1  28133  addsdilem2  28134  mulsasslem1  28145  mulsasslem2  28146  dfcgra2  28885  colinearalg  28966  axcontlem5  29024  nb3grprlem2  29437  wlkeq  29690  isspthonpth  29805  clwlkclwwlklem2a4  30055  clwwlkn1  30099  clwwlkn2  30102  clwwlknon2x  30161  fusgreg2wsp  30394  h2hlm  31038  shlesb1i  31444  pjneli  31781  cnlnssadj  32138  pjin2i  32251  cvnbtwn2  32345  cvnbtwn4  32347  mdsl1i  32379  mdsl2i  32380  hatomistici  32420  cdj3lem3b  32498  iuninc  32617  disjex  32649  disjexc  32650  fpwrelmapffslem  32792  fpwrelmapffs  32794  mgcval  33050  isarchi2  33248  elrgspnlem2  33306  ismntop  34164  coinfliprv  34621  ballotlem2  34627  ballotlemi1  34641  plymulx  34686  oddprm2  34793  bnj168  34867  bnj153  35017  bnj605  35044  bnj607  35053  bnj986  35092  bnj1090  35116  bnj1128  35127  fineqvrep  35251  axregszf  35266  axregs  35276  fmlasucdisj  35574  dfso2  35930  19.12b  35974  dfom5b  36085  elfuns  36088  dfint3  36127  hfext  36358  trer  36491  bj-alcomexcom  36856  wl-3xornot1  37656  wl-df3maxtru1  37668  cnambfre  37840  itg2addnclem2  37844  itg2addnc  37846  heiborlem1  37983  inxpxrn  38590  eldisjdmqsim  38989  lssat  39313  islshpat  39314  lcvnbtwn2  39324  pclfinclN  40247  lhpex2leN  40310  diclspsn  41491  dihmeetlem4preN  41603  dihmeetlem13N  41616  lcdlss  41916  mapd1o  41945  eq0rabdioph  43054  rmspecnonsq  43185  rmxdioph  43294  wopprc  43308  islssfg2  43349  ifpan23  43737  ifpid1g  43771  minregex  43811  dfrtrcl5  43906  dfhe3  44052  ntrneikb  44371  scottabf  44517  2sbc6g  44692  2sbc5g  44693  iotasbc2  44697  2sb5nd  44837  2sb5ndVD  45186  2sb5ndALT  45208  ssclaxsep  45259  permac8prim  45291  limsupre2lem  46004  2rexsb  47383  2rexrsb  47384  usgrexmpl2nb2  48315  usgrexmpl2nb5  48318  usgrexmpl2trifr  48319  islindeps  48735  io1ii  49202