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  828  pm4.15  831  pm5.7  952  pm5.17  1010  pm4.83  1023  3or6  1447  nanim  1496  nannot  1497  empty  1909  19.12vvv  1992  19.12vv  2343  cvjust  2726  necon1abii  2989  nrexralim  3137  r19.23v  3182  nelb  3231  spc3gv  3594  ralxpxfr2d  3634  sbc8g  3785  csbied  3931  ss2rab  4068  difdif  4130  ddif  4136  unass  4166  unss  4184  undi  4274  vn0  4338  ab0orv  4378  disj  4447  disjOLD  4448  ssindif0  4463  prneimg  4855  pwsnOLD  4901  iinrab2  5073  unopab  5230  axrep5  5291  eqvinop  5487  pwssun  5571  dmun  5910  reldm0  5927  dmres  6003  imadmrn  6069  ssrnres  6177  dmsnn0  6206  coundi  6246  coundir  6247  resco  6249  cnvpo  6286  xpco  6288  dfpo2  6295  fun11  6622  fununi  6623  isarep1OLD  6638  fdmrn  6749  dffv2  6986  fsn  7135  eufnfv  7233  eloprabga  7518  eloprabgaOLD  7519  funoprabg  7531  ralrnmpo  7549  imaeqexov  7647  sucexeloniOLD  7800  suceloniOLD  7802  tfinds2  7855  funcnvuni  7924  oprabrexex2  7967  ralxp3f  8125  soseq  8147  dfer2  8706  euen1b  9029  xpsnen  9057  1sdomOLD  9251  wemapsolem  9547  zfregcl  9591  epfrs  9728  rankbnd  9865  rankbnd2  9866  rankxplim2  9877  rankxplim3  9878  isinfcard  10089  dfac5lem2  10121  dfac5lem5  10124  kmlem14  10160  kmlem15  10161  kmlem16  10162  axdc2lem  10445  axcclem  10454  ac9  10480  ac9s  10490  nnunb  12472  xrrebnd  13151  elfznelfzo  13741  hashfun  14401  hashtpg  14450  rexuz3  15299  imasaddfnlem  17478  isnsgrp  18648  eqg0subg  19111  dprd2d2  19955  isnirred  20311  subsubrng2  20452  subsubrg2  20489  isdomn2  21115  mdetunilem8  22341  maducoeval2  22362  tgval2  22679  0top  22706  ssntr  22782  uncmp  23127  opnfbas  23566  fbunfip  23593  alexsubALTlem2  23772  alexsubALTlem3  23773  alexsubALT  23775  metrest  24253  cfilucfil3  25061  ellimc3  25620  plyun0  25935  sinhalfpilem  26197  2lgslem4  27133  addsdilem1  27833  addsdilem2  27834  mulsasslem1  27845  mulsasslem2  27846  dfcgra2  28336  colinearalg  28423  axcontlem5  28481  nb3grprlem2  28893  wlkeq  29146  isspthonpth  29261  clwlkclwwlklem2a4  29505  clwwlkn1  29549  clwwlkn2  29552  clwwlknon2x  29611  fusgreg2wsp  29844  h2hlm  30488  shlesb1i  30894  pjneli  31231  cnlnssadj  31588  pjin2i  31701  cvnbtwn2  31795  cvnbtwn4  31797  mdsl1i  31829  mdsl2i  31830  hatomistici  31870  cdj3lem3b  31948  iuninc  32047  disjex  32078  disjexc  32079  fpwrelmapffslem  32212  fpwrelmapffs  32214  mgcval  32412  isarchi2  32589  ismntop  33292  coinfliprv  33767  ballotlem2  33773  ballotlemi1  33787  plymulx  33845  oddprm2  33953  bnj168  34027  bnj153  34177  bnj605  34204  bnj607  34213  bnj986  34252  bnj1090  34276  bnj1128  34287  fineqvrep  34381  fmlasucdisj  34676  dfso2  35017  19.12b  35065  dfom5b  35176  elfuns  35179  dfint3  35216  hfext  35447  trer  35504  bj-alcomexcom  35861  wl-3xornot1  36664  wl-df3maxtru1  36676  cnambfre  36839  itg2addnclem2  36843  itg2addnc  36845  heiborlem1  36982  inxpxrn  37568  lssat  38189  islshpat  38190  lcvnbtwn2  38200  pclfinclN  39124  lhpex2leN  39187  diclspsn  40368  dihmeetlem4preN  40480  dihmeetlem13N  40493  lcdlss  40793  mapd1o  40822  eq0rabdioph  41816  rmspecnonsq  41947  rmxdioph  42057  wopprc  42071  islssfg2  42115  ifpan23  42513  ifpid1g  42547  minregex  42587  dfrtrcl5  42682  dfhe3  42828  ntrneikb  43147  scottabf  43301  2sbc6g  43476  2sbc5g  43477  iotasbc2  43481  2sb5nd  43623  2sb5ndVD  43973  2sb5ndALT  43995  limsupre2lem  44739  2rexsb  46108  2rexrsb  46109  islindeps  47222  io1ii  47641