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  2345  cvjust  2724  necon1abii  2974  nrexralim  3118  r19.23v  3162  nelb  3214  cbvralsvw  3292  spc3gv  3573  ralxpxfr2d  3615  sbc8g  3764  csbied  3901  dfss2  3935  ss2rab  4037  difdif  4101  ddif  4107  unass  4138  unss  4156  undi  4251  vn0  4311  ab0orv  4349  disj  4416  ssindif0  4430  prneimg  4821  iinrab2  5037  unopab  5190  axrep5  5245  eqvinop  5450  pwssun  5533  dmun  5877  reldm0  5894  dmres  5986  imadmrn  6044  ssrnres  6154  dmsnn0  6183  coundi  6223  coundir  6224  resco  6226  cnvpo  6263  xpco  6265  dfpo2  6272  fun11  6593  fununi  6594  isarep1OLD  6610  fdmrn  6722  dffv2  6959  fsn  7110  eufnfv  7206  eloprabga  7501  funoprabg  7513  ralrnmpo  7531  imaeqexov  7630  sucexeloniOLD  7789  tfinds2  7843  funcnvuni  7911  oprabrexex2  7960  ralxp3f  8119  soseq  8141  dfer2  8675  euen1b  9002  xpsnen  9029  1sdomOLD  9203  wemapsolem  9510  zfregcl  9554  epfrs  9691  rankbnd  9828  rankbnd2  9829  rankxplim2  9840  rankxplim3  9841  isinfcard  10052  dfac5lem2  10084  dfac5lem5  10087  kmlem14  10124  kmlem15  10125  kmlem16  10126  axdc2lem  10408  axcclem  10417  ac9  10443  ac9s  10453  nnunb  12445  xrrebnd  13135  elfznelfzo  13740  hashfun  14409  hashtpg  14457  rexuz3  15322  imasaddfnlem  17498  isnsgrp  18657  eqg0subg  19135  dprd2d2  19983  isnirred  20336  subsubrng2  20480  subsubrg2  20515  isdomn2OLD  20628  mdetunilem8  22513  maducoeval2  22534  tgval2  22850  0top  22877  ssntr  22952  uncmp  23297  opnfbas  23736  fbunfip  23763  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALT  23945  metrest  24419  cfilucfil3  25227  ellimc3  25787  plyun0  26109  sinhalfpilem  26379  2lgslem4  27324  addsdilem1  28061  addsdilem2  28062  mulsasslem1  28073  mulsasslem2  28074  dfcgra2  28764  colinearalg  28844  axcontlem5  28902  nb3grprlem2  29315  wlkeq  29569  isspthonpth  29686  clwlkclwwlklem2a4  29933  clwwlkn1  29977  clwwlkn2  29980  clwwlknon2x  30039  fusgreg2wsp  30272  h2hlm  30916  shlesb1i  31322  pjneli  31659  cnlnssadj  32016  pjin2i  32129  cvnbtwn2  32223  cvnbtwn4  32225  mdsl1i  32257  mdsl2i  32258  hatomistici  32298  cdj3lem3b  32376  iuninc  32496  disjex  32528  disjexc  32529  fpwrelmapffslem  32662  fpwrelmapffs  32664  mgcval  32920  isarchi2  33146  elrgspnlem2  33201  ismntop  34023  coinfliprv  34481  ballotlem2  34487  ballotlemi1  34501  plymulx  34546  oddprm2  34653  bnj168  34727  bnj153  34877  bnj605  34904  bnj607  34913  bnj986  34952  bnj1090  34976  bnj1128  34987  fineqvrep  35092  fmlasucdisj  35393  dfso2  35749  19.12b  35796  dfom5b  35907  elfuns  35910  dfint3  35947  hfext  36178  trer  36311  bj-alcomexcom  36675  wl-3xornot1  37475  wl-df3maxtru1  37487  cnambfre  37669  itg2addnclem2  37673  itg2addnc  37675  heiborlem1  37812  inxpxrn  38388  lssat  39016  islshpat  39017  lcvnbtwn2  39027  pclfinclN  39951  lhpex2leN  40014  diclspsn  41195  dihmeetlem4preN  41307  dihmeetlem13N  41320  lcdlss  41620  mapd1o  41649  eq0rabdioph  42771  rmspecnonsq  42902  rmxdioph  43012  wopprc  43026  islssfg2  43067  ifpan23  43456  ifpid1g  43490  minregex  43530  dfrtrcl5  43625  dfhe3  43771  ntrneikb  44090  scottabf  44236  2sbc6g  44411  2sbc5g  44412  iotasbc2  44416  2sb5nd  44557  2sb5ndVD  44906  2sb5ndALT  44928  ssclaxsep  44979  permac8prim  45011  limsupre2lem  45729  2rexsb  47106  2rexrsb  47107  usgrexmpl2nb2  48028  usgrexmpl2nb5  48031  usgrexmpl2trifr  48032  islindeps  48446  io1ii  48913