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  830  pm4.15  833  pm5.7  956  pm5.17  1014  pm4.83  1027  3or6  1450  nanim  1500  nannot  1501  empty  1908  19.12vvv  1996  19.12vv  2352  cvjust  2731  necon1abii  2981  nrexralim  3122  r19.23v  3165  nelb  3214  cbvralsvw  3289  spc3gv  3547  ralxpxfr2d  3589  sbc8g  3737  csbied  3874  dfss2  3908  ss2rab  4010  difdif  4076  ddif  4082  unass  4113  unss  4131  undi  4226  disj  4391  ssindif0  4405  prneimg  4798  iinrab2  5013  unopab  5166  axrep5  5221  eqvinop  5441  pwssun  5523  dmun  5866  reldm0  5884  dmres  5978  imadmrn  6036  ssrnres  6143  dmsnn0  6172  coundi  6212  coundir  6213  resco  6215  cnvpo  6252  xpco  6254  dfpo2  6261  fun11  6573  fununi  6574  fdmrn  6700  dffv2  6936  fsn  7089  eufnfv  7184  eloprabga  7476  funoprabg  7488  ralrnmpo  7506  imaeqexov  7605  tfinds2  7815  funcnvuni  7883  oprabrexex2  7931  ralxp3f  8087  soseq  8109  dfer2  8644  euen1b  8975  xpsnen  8999  wemapsolem  9465  zfregcl  9509  zfregclOLD  9510  epfrs  9652  rankbnd  9792  rankbnd2  9793  rankxplim2  9804  rankxplim3  9805  isinfcard  10014  dfac5lem2  10046  dfac5lem5  10049  kmlem14  10086  kmlem15  10087  kmlem16  10088  axdc2lem  10370  axcclem  10379  ac9  10405  ac9s  10415  nnunb  12433  xrrebnd  13120  elfznelfzo  13728  hashfun  14399  hashtpg  14447  rexuz3  15311  imasaddfnlem  17492  isnsgrp  18691  eqg0subg  19171  dprd2d2  20021  isnirred  20400  subsubrng2  20541  subsubrg2  20576  isdomn2OLD  20689  mdetunilem8  22584  maducoeval2  22605  tgval2  22921  0top  22948  ssntr  23023  uncmp  23368  opnfbas  23807  fbunfip  23834  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALT  24016  metrest  24489  cfilucfil3  25287  ellimc3  25846  plyun0  26162  sinhalfpilem  26427  2lgslem4  27369  addsdilem1  28143  addsdilem2  28144  mulsasslem1  28155  mulsasslem2  28156  dfcgra2  28898  colinearalg  28979  axcontlem5  29037  nb3grprlem2  29450  wlkeq  29702  isspthonpth  29817  clwlkclwwlklem2a4  30067  clwwlkn1  30111  clwwlkn2  30114  clwwlknon2x  30173  fusgreg2wsp  30406  h2hlm  31051  shlesb1i  31457  pjneli  31794  cnlnssadj  32151  pjin2i  32264  cvnbtwn2  32358  cvnbtwn4  32360  mdsl1i  32392  mdsl2i  32393  hatomistici  32433  cdj3lem3b  32511  iuninc  32630  disjex  32662  disjexc  32663  fpwrelmapffslem  32805  fpwrelmapffs  32807  mgcval  33047  isarchi2  33246  elrgspnlem2  33304  ismntop  34170  coinfliprv  34627  ballotlem2  34633  ballotlemi1  34647  plymulx  34692  oddprm2  34799  bnj168  34873  bnj153  35022  bnj605  35049  bnj607  35058  bnj986  35097  bnj1090  35121  bnj1128  35132  fineqvrep  35258  axregszf  35273  axregs  35283  fmlasucdisj  35581  dfso2  35937  19.12b  35981  dfom5b  36092  elfuns  36095  dfint3  36134  hfext  36365  trer  36498  bj-alcomexcom  36975  wl-3xornot1  37796  wl-df3maxtru1  37808  cnambfre  37989  itg2addnclem2  37993  itg2addnc  37995  heiborlem1  38132  inxpxrn  38739  eldisjdmqsim  39138  lssat  39462  islshpat  39463  lcvnbtwn2  39473  pclfinclN  40396  lhpex2leN  40459  diclspsn  41640  dihmeetlem4preN  41752  dihmeetlem13N  41765  lcdlss  42065  mapd1o  42094  eq0rabdioph  43208  rmspecnonsq  43335  rmxdioph  43444  wopprc  43458  islssfg2  43499  ifpan23  43887  ifpid1g  43921  minregex  43961  dfrtrcl5  44056  dfhe3  44202  ntrneikb  44521  scottabf  44667  2sbc6g  44842  2sbc5g  44843  iotasbc2  44847  2sb5nd  44987  2sb5ndVD  45336  2sb5ndALT  45358  ssclaxsep  45409  permac8prim  45441  limsupre2lem  46152  2rexsb  47543  2rexrsb  47544  usgrexmpl2nb2  48503  usgrexmpl2nb5  48506  usgrexmpl2trifr  48507  islindeps  48923  io1ii  49390