Theorem sylbb 218

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bitri  274  elabgtOLD  3658  ssdifim  4261  ralf0  4515  disjxiun  5146  poclOLD  5598  wefrc  5672  frsn  5765  ssrel  5784  ssrelOLD  5785  funiun  7156  funopsn  7157  ssfi  9198  enfii  9214  nneneq  9234  fissuni  9383  inf3lem2  9654  rankvalb  9822  djur  9944  xrrebnd  13182  xaddf  13238  elfznelfzob  13774  fsuppmapnn0ub  13996  hashinfxadd  14380  hashfun  14432  fz1f1o  15692  dvdszzq  16696  clatl  18503  sgrp2nmndlem5  18889  mat1dimelbas  22417  cfinfil  23841  dyadmax  25571  ausgrusgri  29053  nbupgrres  29249  usgredgsscusgredg  29345  1egrvtxdg0  29397  wlkp1lem7  29565  isch3  31123  nmopun  31896  2ndresdju  32516  cycpm2tr  32932  esumnul  33798  dya2iocnrect  34032  bnj849  34687  bnj1279  34780  cusgr3cyclex  34877  bj-0int  36711  onsucuni3  36977  wl-nfeqfb  37134  poimirlem27  37251  sticksstones20  41769  sucomisnotcard  43116  iunrelexp0  43274  frege129d  43335  clsk3nimkb  43612  gneispace  43706  eliuniin  44605  eliuniin2  44626  stoweidlem48  45574  fourierdlem42  45675  fourierdlem80  45712  eubrdm  46556  oddprmALTV  47164  alimp-no-surprise  48400