Theorem sylbb 220

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  bitri  276  ssdifim  4208  disjxiun  5076  wefrc  5619  frsn  5713  ssrel  5733  funiun  7096  funopsn  7097  funopsnOLD  7098  ssfi  9104  enfii  9117  nneneq  9137  fissuni  9264  inf3lem2  9548  rankvalb  9719  djur  9841  xrrebnd  13118  xaddf  13174  elfznelfzob  13727  fsuppmapnn0ub  13955  hashinfxadd  14345  hashfun  14397  fz1f1o  15670  dvdszzq  16689  clatl  18472  sgrp2nmndlem5  18898  mat1dimelbas  22461  cfinfil  23883  dyadmax  25590  ausgrusgri  29262  nbupgrres  29458  usgredgsscusgredg  29553  1egrvtxdg0  29605  wlkp1lem7  29771  isch3  31337  nmopun  32110  2ndresdju  32748  cycpm2tr  33207  elrgspnlem1  33330  elrgspnlem2  33331  fldextrspunlsplem  33864  esumnul  34239  dya2iocnrect  34472  bnj849  35114  bnj1279  35207  cusgr3cyclex  35371  in-ax8  36459  regsfromunir1  36775  bj-0int  37466  onsucuni3  37736  wl-nfeqfb  37914  poimirlem27  38021  sticksstones20  42658  fimgmcyclem  43026  sucomisnotcard  43995  iunrelexp0  44153  frege129d  44214  clsk3nimkb  44491  gneispace  44585  eliuniin  45553  eliuniin2  45574  stoweidlem48  46498  fourierdlem42  46599  fourierdlem80  46636  eubrdm  47506  oddprmALTV  48185  grtriproplem  48437  grtrif1o  48440  pgnbgreunbgr  48623  alimp-no-surprise  50278