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  3643  ssdifim  4239  ralf0  4480  disjxiun  5107  wefrc  5635  frsn  5729  ssrel  5748  ssrelOLD  5749  funiun  7122  funopsn  7123  ssfi  9143  enfii  9156  nneneq  9176  fissuni  9315  inf3lem2  9589  rankvalb  9757  djur  9879  xrrebnd  13135  xaddf  13191  elfznelfzob  13741  fsuppmapnn0ub  13967  hashinfxadd  14357  hashfun  14409  fz1f1o  15683  dvdszzq  16698  clatl  18474  sgrp2nmndlem5  18863  mat1dimelbas  22365  cfinfil  23787  dyadmax  25506  ausgrusgri  29102  nbupgrres  29298  usgredgsscusgredg  29394  1egrvtxdg0  29446  wlkp1lem7  29614  isch3  31177  nmopun  31950  2ndresdju  32580  cycpm2tr  33083  elrgspnlem1  33200  elrgspnlem2  33201  fldextrspunlsplem  33675  esumnul  34045  dya2iocnrect  34279  bnj849  34922  bnj1279  35015  cusgr3cyclex  35130  in-ax8  36219  bj-0int  37096  onsucuni3  37362  wl-nfeqfb  37531  poimirlem27  37648  sticksstones20  42161  fimgmcyclem  42528  sucomisnotcard  43540  iunrelexp0  43698  frege129d  43759  clsk3nimkb  44036  gneispace  44130  eliuniin  45100  eliuniin2  45121  stoweidlem48  46053  fourierdlem42  46154  fourierdlem80  46191  eubrdm  47041  oddprmALTV  47692  grtriproplem  47942  grtrif1o  47945  pgnbgreunbgr  48119  alimp-no-surprise  49774