Theorem sylbb 221

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 218	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	sylbi 219	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bitri  277  unitreslOLD  874  ssdifim  4242  disjxiun  5066  pocl  5484  wefrc  5552  frsn  5642  ssrel  5660  funiun  6912  funopsn  6913  fissuni  8832  inf3lem2  9095  rankvalb  9229  djur  9351  xrrebnd  12564  xaddf  12620  elfznelfzob  13146  fsuppmapnn0ub  13366  hashinfxadd  13749  hashfun  13801  fz1f1o  15070  clatl  17729  sgrp2nmndlem5  18097  mat1dimelbas  21083  cfinfil  22504  dyadmax  24202  ausgrusgri  26956  nbupgrres  27149  usgredgsscusgredg  27244  1egrvtxdg0  27296  wlkp1lem7  27464  wwlksnfiOLD  27688  isch3  29021  nmopun  29794  dvdszzq  30534  cycpm2tr  30765  esumnul  31311  dya2iocnrect  31543  bnj849  32201  bnj1279  32294  cusgr3cyclex  32387  bj-0int  34397  onsucuni3  34652  wl-nfeqfb  34780  poimirlem27  34923  iunrelexp0  40053  frege129d  40114  clsk3nimkb  40396  gneispace  40490  eliuniin  41371  eliuniin2  41392  stoweidlem48  42340  fourierdlem42  42441  fourierdlem80  42478  eubrdm  43278  oddprmALTV  43859  alimp-no-surprise  44889