Theorem sylbb 222

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bitri  278  ssdifim  4227  disjxiun  5107  wefrc  5657  frsn  5751  ssrel  5771  funiun  7145  funopsn  7146  funopsnOLD  7147  ssfi  9158  enfii  9171  nneneq  9191  fissuni  9315  inf3lem2  9599  rankvalb  9770  djur  9906  xrrebnd  13195  xaddf  13251  elfznelfzob  13805  fsuppmapnn0ub  14033  hashinfxadd  14423  hashfun  14476  fz1f1o  15763  dvdszzq  16781  clatl  18565  sgrp2nmndlem5  18992  mat1dimelbas  22609  cfinfil  24031  dyadmax  25738  ausgrusgri  29496  nbupgrres  29692  usgredgsscusgredg  29787  1egrvtxdg0  29839  wlkp1lem7  30005  isch3  31571  nmopun  32344  2ndresdju  32972  cycpm2tr  33417  elrgspnlem1  33540  elrgspnlem2  33541  fldextrspunlsplem  34041  esumnul  34416  dya2iocnrect  34649  bnj849  35291  bnj1279  35384  rankscott  35500  cusgr3cyclex  35606  in-ax8  36714  regsfromunir1  37029  bj-vn0ALT  37686  bj-0int  37721  onsucuni3  37991  wl-nfeqfb  38169  poimirlem27  38276  sticksstones20  42911  fimgmcyclem  43281  sucomisnotcard  44250  iunrelexp0  44408  frege129d  44469  clsk3nimkb  44746  gneispace  44840  eliuniin  45797  eliuniin2  45818  stoweidlem48  46742  fourierdlem42  46843  fourierdlem80  46880  eubrdm  47750  oddprmALTV  48429  grtriproplem  48681  grtrif1o  48684  pgnbgreunbgr  48867  alimp-no-surprise  50536