Theorem bitr2i 279

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  3bitrri  301  3bitr2ri  303  3bitr4ri  307  nan  842  pm4.15  845  pm5.7  968  pm5.17  1027  pm4.83  1040  3or6  1471  nanim  1521  nannot  1522  empty  1929  19.12vvv  2017  19.12vv  2381  cvjust  2759  necon1abii  3008  nrexralim  3149  r19.23v  3192  nelb  3241  cbvralsvw  3316  spc3gv  3566  ralxpxfr2d  3608  sbc8g  3755  csbied  3891  dfss2  3925  ss2rab  4025  difdif  4091  ddif  4097  unass  4127  unss  4145  undi  4240  disj  4407  ssindif0  4421  prneimg  4815  iinrab2  5030  unopab  5185  axrep5  5240  eqvinop  5460  pwssun  5544  dmun  5891  reldm0  5909  dmres  6002  imadmrn  6063  ssrnres  6168  dmsnn0  6198  coundi  6238  coundir  6239  resco  6241  cnvpo  6278  xpco  6280  dfpo2  6287  fun11  6599  fununi  6600  fdmrn  6727  dffv2  6966  fsn  7121  eufnfv  7217  eloprabga  7509  funoprabg  7521  ralrnmpo  7539  imaeqexov  7638  tfinds2  7848  funcnvuni  7917  oprabrexex2  7963  ralxp3f  8121  soseq  8143  dfer2  8683  euen1b  9013  xpsnen  9037  wemapsolem  9500  zfregcl  9544  zfregclOLD  9545  epfrs  9688  rankbnd  9828  rankbnd2  9829  rankxplim2  9840  rankxplim3  9841  scottabf  9854  isinfcard  10064  dfac5lem2  10096  dfac5lem5  10099  kmlem14  10135  kmlem15  10136  kmlem16  10137  axdc2lem  10420  axcclem  10429  ac9  10455  ac9s  10465  nnunb  12491  xrrebnd  13185  elfznelfzo  13793  hashfun  14464  hashtpg  14512  rexuz3  15390  imasaddfnlem  17572  isnsgrp  18771  eqg0subg  19258  dprd2d2  20107  isnirred  20493  subsubrng2  20640  subsubrg2  20675  mdetunilem8  22737  maducoeval2  22758  tgval2  23074  0top  23101  ssntr  23176  uncmp  23521  opnfbas  23960  fbunfip  23987  alexsubALTlem2  24166  alexsubALTlem3  24167  alexsubALT  24169  metrest  24642  cfilucfil3  25440  ellimc3  25999  plyun0  26315  plymulidp  26404  sinhalfpilem  26586  2lgslem4  27528  addsdilem1  28302  addsdilem2  28303  mulsasslem1  28314  mulsasslem2  28315  dfcgra2  29082  colinearalg  29169  axcontlem5  29227  nb3grprlem2  29640  wlkeq  29892  isspthonpth  30007  clwlkclwwlklem2a4  30257  clwwlkn1  30301  clwwlkn2  30304  clwwlknon2x  30363  fusgreg2wsp  30596  h2hlm  31241  shlesb1i  31647  pjneli  31984  cnlnssadj  32341  pjin2i  32454  cvnbtwn2  32548  cvnbtwn4  32550  mdsl1i  32582  mdsl2i  32583  hatomistici  32623  cdj3lem3b  32701  iuninc  32815  disjex  32847  disjexc  32848  fpwrelmapffslem  32989  fpwrelmapffs  32991  mgcval  33220  isarchi2  33418  elrgspnlem2  33476  ismntop  34333  coinfliprv  34790  ballotlem2  34796  ballotlemi1  34810  oddprm2  34959  bnj168  35036  bnj153  35185  bnj605  35212  bnj607  35221  bnj986  35260  bnj1090  35284  bnj1128  35295  fineqvrep  35422  axregszf  35437  axregs  35447  fmlasucdisj  35762  dfso2  36118  19.12b  36162  dfom5b  36273  elfuns  36276  dfint3  36315  hfext  36546  nmulprop  36553  trer  36689  bj-alcomexcom  37165  wl-3xornot1  37986  wl-df3maxtru1  37998  cnambfre  38179  itg2addnclem2  38183  itg2addnc  38185  heiborlem1  38322  inxpxrn  38929  eldisjdmqsim  39328  lssat  39652  islshpat  39653  lcvnbtwn2  39663  pclfinclN  40586  lhpex2leN  40649  diclspsn  41830  dihmeetlem4preN  41942  dihmeetlem13N  41955  lcdlss  42255  mapd1o  42284  eq0rabdioph  43369  rmspecnonsq  43496  rmxdioph  43605  wopprc  43619  islssfg2  43660  ifpan23  44048  ifpid1g  44082  minregex  44122  dfrtrcl5  44217  dfhe3  44363  ntrneikb  44682  2sbc6g  44989  2sbc5g  44990  iotasbc2  44994  2sb5nd  45134  2sb5ndVD  45483  2sb5ndALT  45505  ssclaxsep  45556  permac8prim  45588  limsupre2lem  46296  2rexsb  47693  2rexrsb  47694  usgrexmpl2nb2  48653  usgrexmpl2nb5  48656  usgrexmpl2trifr  48657  islindeps  49084  io1ii  49550