Theorem sylbb 219

Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 30-Mar-2019.)

Hypotheses

Ref	Expression
sylbb.1	⊢ (𝜑 ↔ 𝜓)
sylbb.2	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
sylbb	⊢ (𝜑 → 𝜒)

Proof of Theorem sylbb

Step	Hyp	Ref	Expression
1		sylbb.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		sylbb.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3	2	biimpi 216	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	sylbi 217	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ 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:  bitri  275  elabgtOLDOLD  3631  ssdifim  4226  ralf0  4467  disjxiun  5092  wefrc  5617  frsn  5711  ssrel  5730  funiun  7085  funopsn  7086  ssfi  9097  enfii  9110  nneneq  9130  fissuni  9266  inf3lem2  9544  rankvalb  9712  djur  9834  xrrebnd  13088  xaddf  13144  elfznelfzob  13694  fsuppmapnn0ub  13920  hashinfxadd  14310  hashfun  14362  fz1f1o  15635  dvdszzq  16650  clatl  18432  sgrp2nmndlem5  18821  mat1dimelbas  22374  cfinfil  23796  dyadmax  25515  ausgrusgri  29131  nbupgrres  29327  usgredgsscusgredg  29423  1egrvtxdg0  29475  wlkp1lem7  29641  isch3  31203  nmopun  31976  2ndresdju  32606  cycpm2tr  33074  elrgspnlem1  33192  elrgspnlem2  33193  fldextrspunlsplem  33644  esumnul  34014  dya2iocnrect  34248  bnj849  34891  bnj1279  34984  cusgr3cyclex  35108  in-ax8  36197  bj-0int  37074  onsucuni3  37340  wl-nfeqfb  37509  poimirlem27  37626  sticksstones20  42139  fimgmcyclem  42506  sucomisnotcard  43517  iunrelexp0  43675  frege129d  43736  clsk3nimkb  44013  gneispace  44107  eliuniin  45077  eliuniin2  45098  stoweidlem48  46030  fourierdlem42  46131  fourierdlem80  46168  eubrdm  47021  oddprmALTV  47672  grtriproplem  47924  grtrif1o  47927  pgnbgreunbgr  48110  alimp-no-surprise  49767