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  2725  necon1abii  2988  nabbi  3044  nrexralim  3130  r19.23v  3175  nelb  3220  spc3gv  3564  ralxpxfr2d  3599  sbc8g  3750  csbied  3896  ss2rab  4033  difdif  4095  ddif  4101  unass  4131  unss  4149  undi  4239  vn0  4303  ab0orv  4343  disj  4412  disjOLD  4413  ssindif0  4428  prneimg  4817  pwsnOLD  4863  iinrab2  5035  unopab  5192  axrep5  5253  eqvinop  5449  pwssun  5533  dmun  5871  reldm0  5888  dmres  5964  imadmrn  6028  ssrnres  6135  dmsnn0  6164  coundi  6204  coundir  6205  resco  6207  cnvpo  6244  xpco  6246  dfpo2  6253  fun11  6580  fununi  6581  isarep1OLD  6596  fdmrn  6705  dffv2  6941  fsn  7086  eufnfv  7184  eloprabga  7469  eloprabgaOLD  7470  funoprabg  7482  ralrnmpo  7499  imaeqexov  7597  sucexeloniOLD  7750  suceloniOLD  7752  tfinds2  7805  funcnvuni  7873  oprabrexex2  7916  ralxp3f  8074  soseq  8096  dfer2  8656  euen1b  8978  xpsnen  9006  1sdomOLD  9200  wemapsolem  9495  zfregcl  9539  epfrs  9676  rankbnd  9813  rankbnd2  9814  rankxplim2  9825  rankxplim3  9826  isinfcard  10037  dfac5lem2  10069  dfac5lem5  10072  kmlem14  10108  kmlem15  10109  kmlem16  10110  axdc2lem  10393  axcclem  10402  ac9  10428  ac9s  10438  nnunb  12418  xrrebnd  13097  elfznelfzo  13687  hashfun  14347  hashtpg  14396  rexuz3  15245  imasaddfnlem  17424  isnsgrp  18564  dprd2d2  19837  isnirred  20145  subsubrg2  20298  isdomn2  20806  mdetunilem8  22005  maducoeval2  22026  tgval2  22343  0top  22370  ssntr  22446  uncmp  22791  opnfbas  23230  fbunfip  23257  alexsubALTlem2  23436  alexsubALTlem3  23437  alexsubALT  23439  metrest  23917  cfilucfil3  24721  ellimc3  25280  plyun0  25595  sinhalfpilem  25857  2lgslem4  26791  dfcgra2  27835  colinearalg  27922  axcontlem5  27980  nb3grprlem2  28392  wlkeq  28645  isspthonpth  28760  clwlkclwwlklem2a4  29004  clwwlkn1  29048  clwwlkn2  29051  clwwlknon2x  29110  fusgreg2wsp  29343  h2hlm  29985  shlesb1i  30391  pjneli  30728  cnlnssadj  31085  pjin2i  31198  cvnbtwn2  31292  cvnbtwn4  31294  mdsl1i  31326  mdsl2i  31327  hatomistici  31367  cdj3lem3b  31445  iuninc  31546  disjex  31577  disjexc  31578  fpwrelmapffslem  31717  fpwrelmapffs  31719  mgcval  31917  isarchi2  32091  ismntop  32696  coinfliprv  33171  ballotlem2  33177  ballotlemi1  33191  plymulx  33249  oddprm2  33357  bnj168  33431  bnj153  33581  bnj605  33608  bnj607  33617  bnj986  33656  bnj1090  33680  bnj1128  33691  fineqvrep  33785  fmlasucdisj  34080  dfso2  34414  19.12b  34462  dfom5b  34573  elfuns  34576  dfint3  34613  hfext  34844  trer  34864  bj-alcomexcom  35221  wl-3xornot1  36024  wl-df3maxtru1  36036  cnambfre  36199  itg2addnclem2  36203  itg2addnc  36205  heiborlem1  36343  inxpxrn  36930  lssat  37551  islshpat  37552  lcvnbtwn2  37562  pclfinclN  38486  lhpex2leN  38549  diclspsn  39730  dihmeetlem4preN  39842  dihmeetlem13N  39855  lcdlss  40155  mapd1o  40184  eq0rabdioph  41157  rmspecnonsq  41288  rmxdioph  41398  wopprc  41412  islssfg2  41456  ifpan23  41854  ifpid1g  41888  minregex  41928  dfrtrcl5  42023  dfhe3  42169  ntrneikb  42488  scottabf  42642  2sbc6g  42817  2sbc5g  42818  iotasbc2  42822  2sb5nd  42964  2sb5ndVD  43314  2sb5ndALT  43336  limsupre2lem  44085  2rexsb  45453  2rexrsb  45454  islindeps  46654  io1ii  47073