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  3617  ssdifim  4214  disjxiun  5083  wefrc  5618  frsn  5712  ssrel  5732  funiun  7094  funopsn  7095  ssfi  9100  enfii  9113  nneneq  9133  fissuni  9260  inf3lem2  9541  rankvalb  9712  djur  9834  xrrebnd  13111  xaddf  13167  elfznelfzob  13720  fsuppmapnn0ub  13948  hashinfxadd  14338  hashfun  14390  fz1f1o  15663  dvdszzq  16682  clatl  18465  sgrp2nmndlem5  18891  mat1dimelbas  22446  cfinfil  23868  dyadmax  25575  ausgrusgri  29251  nbupgrres  29447  usgredgsscusgredg  29543  1egrvtxdg0  29595  wlkp1lem7  29761  isch3  31327  nmopun  32100  2ndresdju  32737  cycpm2tr  33195  elrgspnlem1  33318  elrgspnlem2  33319  fldextrspunlsplem  33833  esumnul  34208  dya2iocnrect  34441  bnj849  35083  bnj1279  35176  cusgr3cyclex  35334  in-ax8  36422  regsfromunir1  36738  bj-0int  37429  onsucuni3  37697  wl-nfeqfb  37875  poimirlem27  37982  sticksstones20  42619  fimgmcyclem  42992  sucomisnotcard  43989  iunrelexp0  44147  frege129d  44208  clsk3nimkb  44485  gneispace  44579  eliuniin  45547  eliuniin2  45568  stoweidlem48  46494  fourierdlem42  46595  fourierdlem80  46632  eubrdm  47496  oddprmALTV  48175  grtriproplem  48427  grtrif1o  48430  pgnbgreunbgr  48613  alimp-no-surprise  50268