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  3630  ssdifim  4227  disjxiun  5097  wefrc  5626  frsn  5720  ssrel  5740  funiun  7102  funopsn  7103  ssfi  9109  enfii  9122  nneneq  9142  fissuni  9269  inf3lem2  9550  rankvalb  9721  djur  9843  xrrebnd  13095  xaddf  13151  elfznelfzob  13702  fsuppmapnn0ub  13930  hashinfxadd  14320  hashfun  14372  fz1f1o  15645  dvdszzq  16660  clatl  18443  sgrp2nmndlem5  18866  mat1dimelbas  22427  cfinfil  23849  dyadmax  25567  ausgrusgri  29253  nbupgrres  29449  usgredgsscusgredg  29545  1egrvtxdg0  29597  wlkp1lem7  29763  isch3  31328  nmopun  32101  2ndresdju  32738  cycpm2tr  33212  elrgspnlem1  33335  elrgspnlem2  33336  fldextrspunlsplem  33850  esumnul  34225  dya2iocnrect  34458  bnj849  35100  bnj1279  35193  cusgr3cyclex  35349  in-ax8  36437  regsfromunir1  36689  bj-0int  37348  onsucuni3  37616  wl-nfeqfb  37785  poimirlem27  37892  sticksstones20  42530  fimgmcyclem  42897  sucomisnotcard  43894  iunrelexp0  44052  frege129d  44113  clsk3nimkb  44390  gneispace  44484  eliuniin  45452  eliuniin2  45473  stoweidlem48  46400  fourierdlem42  46501  fourierdlem80  46538  eubrdm  47390  oddprmALTV  48041  grtriproplem  48293  grtrif1o  48296  pgnbgreunbgr  48479  alimp-no-surprise  50134