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  1499  nannot  1500  empty  1907  19.12vvv  1995  19.12vv  2349  cvjust  2727  necon1abii  2978  nrexralim  3118  r19.23v  3161  nelb  3210  cbvralsvw  3285  spc3gv  3556  ralxpxfr2d  3598  sbc8g  3746  csbied  3883  dfss2  3917  ss2abim  4010  ss2rab  4019  difdif  4086  ddif  4092  unass  4123  unss  4141  undi  4236  disj  4401  ssindif0  4415  prneimg  4807  iinrab2  5022  unopab  5175  axrep5  5229  eqvinop  5432  pwssun  5513  dmun  5857  reldm0  5875  dmres  5968  imadmrn  6026  ssrnres  6133  dmsnn0  6162  coundi  6202  coundir  6203  resco  6205  cnvpo  6242  xpco  6244  dfpo2  6251  fun11  6563  fununi  6564  fdmrn  6690  dffv2  6926  fsn  7077  eufnfv  7172  eloprabga  7464  funoprabg  7476  ralrnmpo  7494  imaeqexov  7593  tfinds2  7803  funcnvuni  7871  oprabrexex2  7919  ralxp3f  8076  soseq  8098  dfer2  8632  euen1b  8960  xpsnen  8984  wemapsolem  9446  zfregcl  9490  zfregclOLD  9491  epfrs  9631  rankbnd  9771  rankbnd2  9772  rankxplim2  9783  rankxplim3  9784  isinfcard  9993  dfac5lem2  10025  dfac5lem5  10028  kmlem14  10065  kmlem15  10066  kmlem16  10067  axdc2lem  10349  axcclem  10358  ac9  10384  ac9s  10394  nnunb  12387  xrrebnd  13077  elfznelfzo  13683  hashfun  14354  hashtpg  14402  rexuz3  15266  imasaddfnlem  17442  isnsgrp  18641  eqg0subg  19118  dprd2d2  19968  isnirred  20348  subsubrng2  20489  subsubrg2  20524  isdomn2OLD  20637  mdetunilem8  22544  maducoeval2  22565  tgval2  22881  0top  22908  ssntr  22983  uncmp  23328  opnfbas  23767  fbunfip  23794  alexsubALTlem2  23973  alexsubALTlem3  23974  alexsubALT  23976  metrest  24449  cfilucfil3  25257  ellimc3  25817  plyun0  26139  sinhalfpilem  26409  2lgslem4  27354  addsdilem1  28100  addsdilem2  28101  mulsasslem1  28112  mulsasslem2  28113  dfcgra2  28818  colinearalg  28899  axcontlem5  28957  nb3grprlem2  29370  wlkeq  29623  isspthonpth  29738  clwlkclwwlklem2a4  29988  clwwlkn1  30032  clwwlkn2  30035  clwwlknon2x  30094  fusgreg2wsp  30327  h2hlm  30971  shlesb1i  31377  pjneli  31714  cnlnssadj  32071  pjin2i  32184  cvnbtwn2  32278  cvnbtwn4  32280  mdsl1i  32312  mdsl2i  32313  hatomistici  32353  cdj3lem3b  32431  iuninc  32551  disjex  32583  disjexc  32584  fpwrelmapffslem  32726  fpwrelmapffs  32728  mgcval  32979  isarchi2  33165  elrgspnlem2  33221  ismntop  34050  coinfliprv  34507  ballotlem2  34513  ballotlemi1  34527  plymulx  34572  oddprm2  34679  bnj168  34753  bnj153  34903  bnj605  34930  bnj607  34939  bnj986  34978  bnj1090  35002  bnj1128  35013  axregszf  35138  fineqvrep  35148  axregs  35156  fmlasucdisj  35454  dfso2  35810  19.12b  35854  dfom5b  35965  elfuns  35968  dfint3  36007  hfext  36238  trer  36371  bj-alcomexcom  36735  wl-3xornot1  37535  wl-df3maxtru1  37547  cnambfre  37718  itg2addnclem2  37722  itg2addnc  37724  heiborlem1  37861  inxpxrn  38452  lssat  39125  islshpat  39126  lcvnbtwn2  39136  pclfinclN  40059  lhpex2leN  40122  diclspsn  41303  dihmeetlem4preN  41415  dihmeetlem13N  41428  lcdlss  41728  mapd1o  41757  eq0rabdioph  42883  rmspecnonsq  43014  rmxdioph  43123  wopprc  43137  islssfg2  43178  ifpan23  43567  ifpid1g  43601  minregex  43641  dfrtrcl5  43736  dfhe3  43882  ntrneikb  44201  scottabf  44347  2sbc6g  44522  2sbc5g  44523  iotasbc2  44527  2sb5nd  44667  2sb5ndVD  45016  2sb5ndALT  45038  ssclaxsep  45089  permac8prim  45121  limsupre2lem  45836  2rexsb  47215  2rexrsb  47216  usgrexmpl2nb2  48147  usgrexmpl2nb5  48150  usgrexmpl2trifr  48151  islindeps  48568  io1ii  49035