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  3628  ssdifim  4225  disjxiun  5095  wefrc  5618  frsn  5712  ssrel  5732  funiun  7092  funopsn  7093  ssfi  9097  enfii  9110  nneneq  9130  fissuni  9257  inf3lem2  9538  rankvalb  9709  djur  9831  xrrebnd  13083  xaddf  13139  elfznelfzob  13690  fsuppmapnn0ub  13918  hashinfxadd  14308  hashfun  14360  fz1f1o  15633  dvdszzq  16648  clatl  18431  sgrp2nmndlem5  18854  mat1dimelbas  22415  cfinfil  23837  dyadmax  25555  ausgrusgri  29241  nbupgrres  29437  usgredgsscusgredg  29533  1egrvtxdg0  29585  wlkp1lem7  29751  isch3  31316  nmopun  32089  2ndresdju  32727  cycpm2tr  33201  elrgspnlem1  33324  elrgspnlem2  33325  fldextrspunlsplem  33830  esumnul  34205  dya2iocnrect  34438  bnj849  35081  bnj1279  35174  cusgr3cyclex  35330  in-ax8  36418  regsfromunir1  36670  bj-0int  37302  onsucuni3  37568  wl-nfeqfb  37737  poimirlem27  37844  sticksstones20  42416  fimgmcyclem  42784  sucomisnotcard  43781  iunrelexp0  43939  frege129d  44000  clsk3nimkb  44277  gneispace  44371  eliuniin  45339  eliuniin2  45360  stoweidlem48  46288  fourierdlem42  46389  fourierdlem80  46426  eubrdm  47278  oddprmALTV  47929  grtriproplem  48181  grtrif1o  48184  pgnbgreunbgr  48367  alimp-no-surprise  50022