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  3652  ssdifim  4248  ralf0  4489  disjxiun  5116  wefrc  5648  frsn  5742  ssrel  5761  ssrelOLD  5762  funiun  7136  funopsn  7137  ssfi  9185  enfii  9198  nneneq  9218  fissuni  9367  inf3lem2  9641  rankvalb  9809  djur  9931  xrrebnd  13182  xaddf  13238  elfznelfzob  13787  fsuppmapnn0ub  14011  hashinfxadd  14401  hashfun  14453  fz1f1o  15724  dvdszzq  16738  clatl  18516  sgrp2nmndlem5  18905  mat1dimelbas  22407  cfinfil  23829  dyadmax  25549  ausgrusgri  29093  nbupgrres  29289  usgredgsscusgredg  29385  1egrvtxdg0  29437  wlkp1lem7  29605  isch3  31168  nmopun  31941  2ndresdju  32573  cycpm2tr  33076  elrgspnlem1  33183  elrgspnlem2  33184  fldextrspunlsplem  33660  esumnul  34025  dya2iocnrect  34259  bnj849  34902  bnj1279  34995  cusgr3cyclex  35104  in-ax8  36188  bj-0int  37065  onsucuni3  37331  wl-nfeqfb  37500  poimirlem27  37617  sticksstones20  42125  fimgmcyclem  42503  sucomisnotcard  43515  iunrelexp0  43673  frege129d  43734  clsk3nimkb  44011  gneispace  44105  eliuniin  45071  eliuniin2  45092  stoweidlem48  46025  fourierdlem42  46126  fourierdlem80  46163  eubrdm  47013  oddprmALTV  47649  grtriproplem  47899  grtrif1o  47902  alimp-no-surprise  49593