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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bitri  278  ssdifim  4219  disjxiun  5100  wefrc  5645  frsn  5739  ssrel  5759  funiun  7142  funopsn  7143  funopsnOLD  7144  ssfi  9172  enfii  9185  nneneq  9205  fissuni  9330  inf3lem2  9614  rankvalb  9787  hffi  9890  djur  9981  xrrebnd  13279  xaddf  13335  elfznelfzob  13889  fsuppmapnn0ub  14118  hashinfxadd  14509  hashfun  14562  fz1f1o  15856  dvdszzq  16877  clatl  18662  sgrp2nmndlem5  19108  mat1dimelbas  22766  cfinfil  24192  dyadmax  25899  ausgrusgri  29731  nbupgrres  29927  usgredgsscusgredg  30022  1egrvtxdg0  30074  wlkp1lem7  30240  isch3  31825  nmopun  32598  2ndresdju  33225  cycpm2tr  33662  elrgspnlem1  33785  elrgspnlem2  33786  fldextrspunlsplem  34287  esumnul  34662  dya2iocnrect  34896  bnj849  35538  bnj1279  35631  rankscott  35730  cusgr3cyclex  35880  in-ax8  36983  regsfromunir1  37298  bj-vn0ALT  37955  bj-0int  37990  onsucuni3  38258  wl-nfeqfb  38436  poimirlem27  38533  sticksstones20  43184  fimgmcyclem  43559  sucomisnotcard  44503  iunrelexp0  44661  frege129d  44722  clsk3nimkb  44999  gneispace  45093  eliuniin  46057  eliuniin2  46078  stoweidlem48  47002  fourierdlem42  47103  fourierdlem80  47140  eubrdm  48050  oddprmALTV  48729  grtriproplem  48981  grtrif1o  48984  pgnbgreunbgr  49167  alimp-no-surprise  50821