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  elabgtOLDOLD  3625  ssdifim  4222  ralf0  4463  disjxiun  5090  wefrc  5613  frsn  5707  ssrel  5727  funiun  7086  funopsn  7087  ssfi  9089  enfii  9102  nneneq  9122  fissuni  9248  inf3lem2  9526  rankvalb  9697  djur  9819  xrrebnd  13069  xaddf  13125  elfznelfzob  13676  fsuppmapnn0ub  13904  hashinfxadd  14294  hashfun  14346  fz1f1o  15619  dvdszzq  16634  clatl  18416  sgrp2nmndlem5  18839  mat1dimelbas  22387  cfinfil  23809  dyadmax  25527  ausgrusgri  29148  nbupgrres  29344  usgredgsscusgredg  29440  1egrvtxdg0  29492  wlkp1lem7  29658  isch3  31223  nmopun  31996  2ndresdju  32633  cycpm2tr  33095  elrgspnlem1  33216  elrgspnlem2  33217  fldextrspunlsplem  33707  esumnul  34082  dya2iocnrect  34315  bnj849  34958  bnj1279  35051  cusgr3cyclex  35201  in-ax8  36289  bj-0int  37166  onsucuni3  37432  wl-nfeqfb  37601  poimirlem27  37707  sticksstones20  42279  fimgmcyclem  42651  sucomisnotcard  43661  iunrelexp0  43819  frege129d  43880  clsk3nimkb  44157  gneispace  44251  eliuniin  45220  eliuniin2  45241  stoweidlem48  46170  fourierdlem42  46271  fourierdlem80  46308  eubrdm  47160  oddprmALTV  47811  grtriproplem  48063  grtrif1o  48066  pgnbgreunbgr  48249  alimp-no-surprise  49906