Theorem bitr2i 275

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 274	. 2 ⊢ (𝜑 ↔ 𝜒)
4	3	bicomi 223	1 ⊢ (𝜒 ↔ 𝜑)

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  3bitrri  297  3bitr2ri  299  3bitr4ri  303  nan  826  pm4.15  829  pm5.7  950  pm5.17  1008  pm4.83  1021  3or6  1445  nanim  1490  nannot  1491  empty  1910  19.12vvv  1993  19.12vv  2347  cvjust  2732  abbi  2811  abbiOLD  2879  necon1abii  2991  nabbi  3046  nrexralim  3192  nelb  3194  r19.23v  3207  spc3gv  3533  ralxpxfr2d  3568  sbc8g  3719  csbied  3866  ss2rab  4000  difdif  4061  ddif  4067  unass  4096  unss  4114  undi  4205  vn0  4269  ab0orv  4309  disj  4378  disjOLD  4379  ssindif0  4394  prneimg  4782  pwsnOLD  4829  iinrab2  4995  unopab  5152  axrep5  5211  eqvinop  5395  pwssun  5476  dmun  5808  reldm0  5826  dmres  5902  imadmrn  5968  ssrnres  6070  dmsnn0  6099  coundi  6140  coundir  6141  resco  6143  cnvpo  6179  xpco  6181  dfpo2  6188  fun11  6492  fununi  6493  isarep1  6506  fdmrn  6616  dffv2  6845  fsn  6989  eufnfv  7087  eloprabga  7360  eloprabgaOLD  7361  funoprabg  7373  ralrnmpo  7390  suceloni  7635  tfinds2  7685  funcnvuni  7752  oprabrexex2  7794  fsplitOLD  7929  dfer2  8457  euen1b  8771  xpsnen  8796  1sdom  8955  wemapsolem  9239  zfregcl  9283  epfrs  9420  rankbnd  9557  rankbnd2  9558  rankxplim2  9569  rankxplim3  9570  isinfcard  9779  dfac5lem2  9811  dfac5lem5  9814  kmlem14  9850  kmlem15  9851  kmlem16  9852  axdc2lem  10135  axcclem  10144  ac9  10170  ac9s  10180  nnunb  12159  xrrebnd  12831  elfznelfzo  13420  hashfun  14080  hashtpg  14127  rexuz3  14988  imasaddfnlem  17156  isnsgrp  18294  dprd2d2  19562  isnirred  19857  subsubrg2  19966  isdomn2  20483  mdetunilem8  21676  maducoeval2  21697  tgval2  22014  0top  22041  ssntr  22117  uncmp  22462  opnfbas  22901  fbunfip  22928  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALT  23110  metrest  23586  cfilucfil3  24389  ellimc3  24948  plyun0  25263  sinhalfpilem  25525  2lgslem4  26459  dfcgra2  27095  colinearalg  27181  axcontlem5  27239  nb3grprlem2  27651  wlkeq  27903  isspthonpth  28018  clwlkclwwlklem2a4  28262  clwwlkn1  28306  clwwlkn2  28309  clwwlknon2x  28368  fusgreg2wsp  28601  h2hlm  29243  shlesb1i  29649  pjneli  29986  cnlnssadj  30343  pjin2i  30456  cvnbtwn2  30550  cvnbtwn4  30552  mdsl1i  30584  mdsl2i  30585  hatomistici  30625  cdj3lem3b  30703  nelbOLDOLD  30718  iuninc  30801  disjex  30832  disjexc  30833  fpwrelmapffslem  30969  fpwrelmapffs  30971  mgcval  31167  isarchi2  31341  ismntop  31876  coinfliprv  32349  ballotlem2  32355  ballotlemi1  32369  plymulx  32427  oddprm2  32535  bnj168  32609  bnj153  32760  bnj605  32787  bnj607  32796  bnj986  32835  bnj1090  32859  bnj1128  32870  fineqvrep  32964  fmlasucdisj  33261  dfso2  33628  19.12b  33683  xpord3ind  33727  soseq  33730  dfom5b  34141  elfuns  34144  dfint3  34181  hfext  34412  trer  34432  wl-3xornot1  35578  wl-df3maxtru1  35590  cnambfre  35752  itg2addnclem2  35756  itg2addnc  35758  heiborlem1  35896  inxpxrn  36448  lssat  36957  islshpat  36958  lcvnbtwn2  36968  pclfinclN  37891  lhpex2leN  37954  diclspsn  39135  dihmeetlem4preN  39247  dihmeetlem13N  39260  lcdlss  39560  mapd1o  39589  eq0rabdioph  40514  rmspecnonsq  40645  rmxdioph  40754  wopprc  40768  islssfg2  40812  ifpan23  40965  ifpid1g  40999  dfrtrcl5  41126  dfhe3  41272  ntrneikb  41593  scottabf  41747  2sbc6g  41922  2sbc5g  41923  iotasbc2  41927  2sb5nd  42069  2sb5ndVD  42419  2sb5ndALT  42441  limsupre2lem  43155  2rexsb  44480  2rexrsb  44481  islindeps  45682  io1ii  46102