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  elabgtOLD  3686  ssdifim  4292  ralf0  4537  disjxiun  5163  poclOLD  5616  wefrc  5694  frsn  5787  ssrel  5806  ssrelOLD  5807  funiun  7181  funopsn  7182  ssfi  9240  enfii  9252  nneneq  9272  fissuni  9427  inf3lem2  9698  rankvalb  9866  djur  9988  xrrebnd  13230  xaddf  13286  elfznelfzob  13823  fsuppmapnn0ub  14046  hashinfxadd  14434  hashfun  14486  fz1f1o  15758  dvdszzq  16768  clatl  18578  sgrp2nmndlem5  18964  mat1dimelbas  22498  cfinfil  23922  dyadmax  25652  ausgrusgri  29203  nbupgrres  29399  usgredgsscusgredg  29495  1egrvtxdg0  29547  wlkp1lem7  29715  isch3  31273  nmopun  32046  2ndresdju  32667  cycpm2tr  33112  esumnul  34012  dya2iocnrect  34246  bnj849  34901  bnj1279  34994  cusgr3cyclex  35104  in-ax8  36190  bj-0int  37067  onsucuni3  37333  wl-nfeqfb  37490  poimirlem27  37607  sticksstones20  42123  fimgmcyclem  42488  sucomisnotcard  43506  iunrelexp0  43664  frege129d  43725  clsk3nimkb  44002  gneispace  44096  eliuniin  45001  eliuniin2  45022  stoweidlem48  45969  fourierdlem42  46070  fourierdlem80  46107  eubrdm  46951  oddprmALTV  47561  grtriproplem  47790  grtrif1o  47793  alimp-no-surprise  48875