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 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  298  3bitr2ri  300  3bitr4ri  304  nan  829  pm4.15  832  pm5.7  953  pm5.17  1011  pm4.83  1024  3or6  1448  nanim  1497  nannot  1498  empty  1910  19.12vvv  1993  19.12vv  2344  cvjust  2727  necon1abii  2990  nrexralim  3138  r19.23v  3183  nelb  3232  spc3gv  3595  ralxpxfr2d  3635  sbc8g  3786  csbied  3932  ss2rab  4069  difdif  4131  ddif  4137  unass  4167  unss  4185  undi  4275  vn0  4339  ab0orv  4379  disj  4448  disjOLD  4449  ssindif0  4464  prneimg  4856  pwsnOLD  4902  iinrab2  5074  unopab  5231  axrep5  5292  eqvinop  5488  pwssun  5572  dmun  5911  reldm0  5928  dmres  6004  imadmrn  6070  ssrnres  6178  dmsnn0  6207  coundi  6247  coundir  6248  resco  6250  cnvpo  6287  xpco  6289  dfpo2  6296  fun11  6623  fununi  6624  isarep1OLD  6639  fdmrn  6750  dffv2  6987  fsn  7133  eufnfv  7231  eloprabga  7516  eloprabgaOLD  7517  funoprabg  7529  ralrnmpo  7547  imaeqexov  7645  sucexeloniOLD  7798  suceloniOLD  7800  tfinds2  7853  funcnvuni  7922  oprabrexex2  7965  ralxp3f  8123  soseq  8145  dfer2  8704  euen1b  9027  xpsnen  9055  1sdomOLD  9249  wemapsolem  9545  zfregcl  9589  epfrs  9726  rankbnd  9863  rankbnd2  9864  rankxplim2  9875  rankxplim3  9876  isinfcard  10087  dfac5lem2  10119  dfac5lem5  10122  kmlem14  10158  kmlem15  10159  kmlem16  10160  axdc2lem  10443  axcclem  10452  ac9  10478  ac9s  10488  nnunb  12468  xrrebnd  13147  elfznelfzo  13737  hashfun  14397  hashtpg  14446  rexuz3  15295  imasaddfnlem  17474  isnsgrp  18614  eqg0subg  19073  dprd2d2  19914  isnirred  20234  subsubrg2  20346  isdomn2  20915  mdetunilem8  22121  maducoeval2  22142  tgval2  22459  0top  22486  ssntr  22562  uncmp  22907  opnfbas  23346  fbunfip  23373  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALT  23555  metrest  24033  cfilucfil3  24837  ellimc3  25396  plyun0  25711  sinhalfpilem  25973  2lgslem4  26909  addsdilem1  27609  addsdilem2  27610  mulsasslem1  27621  mulsasslem2  27622  dfcgra2  28112  colinearalg  28199  axcontlem5  28257  nb3grprlem2  28669  wlkeq  28922  isspthonpth  29037  clwlkclwwlklem2a4  29281  clwwlkn1  29325  clwwlkn2  29328  clwwlknon2x  29387  fusgreg2wsp  29620  h2hlm  30264  shlesb1i  30670  pjneli  31007  cnlnssadj  31364  pjin2i  31477  cvnbtwn2  31571  cvnbtwn4  31573  mdsl1i  31605  mdsl2i  31606  hatomistici  31646  cdj3lem3b  31724  iuninc  31823  disjex  31854  disjexc  31855  fpwrelmapffslem  31988  fpwrelmapffs  31990  mgcval  32188  isarchi2  32362  ismntop  33037  coinfliprv  33512  ballotlem2  33518  ballotlemi1  33532  plymulx  33590  oddprm2  33698  bnj168  33772  bnj153  33922  bnj605  33949  bnj607  33958  bnj986  33997  bnj1090  34021  bnj1128  34032  fineqvrep  34126  fmlasucdisj  34421  dfso2  34756  19.12b  34804  dfom5b  34915  elfuns  34918  dfint3  34955  hfext  35186  trer  35249  bj-alcomexcom  35606  wl-3xornot1  36409  wl-df3maxtru1  36421  cnambfre  36584  itg2addnclem2  36588  itg2addnc  36590  heiborlem1  36727  inxpxrn  37313  lssat  37934  islshpat  37935  lcvnbtwn2  37945  pclfinclN  38869  lhpex2leN  38932  diclspsn  40113  dihmeetlem4preN  40225  dihmeetlem13N  40238  lcdlss  40538  mapd1o  40567  eq0rabdioph  41562  rmspecnonsq  41693  rmxdioph  41803  wopprc  41817  islssfg2  41861  ifpan23  42259  ifpid1g  42293  minregex  42333  dfrtrcl5  42428  dfhe3  42574  ntrneikb  42893  scottabf  43047  2sbc6g  43222  2sbc5g  43223  iotasbc2  43227  2sb5nd  43369  2sb5ndVD  43719  2sb5ndALT  43741  limsupre2lem  44488  2rexsb  45857  2rexrsb  45858  subsubrng2  46791  islindeps  47182  io1ii  47601