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  3616  ssdifim  4213  disjxiun  5082  wefrc  5625  frsn  5719  ssrel  5739  funiun  7100  funopsn  7101  funopsnOLD  7102  ssfi  9107  enfii  9120  nneneq  9140  fissuni  9267  inf3lem2  9550  rankvalb  9721  djur  9843  xrrebnd  13120  xaddf  13176  elfznelfzob  13729  fsuppmapnn0ub  13957  hashinfxadd  14347  hashfun  14399  fz1f1o  15672  dvdszzq  16691  clatl  18474  sgrp2nmndlem5  18900  mat1dimelbas  22436  cfinfil  23858  dyadmax  25565  ausgrusgri  29237  nbupgrres  29433  usgredgsscusgredg  29528  1egrvtxdg0  29580  wlkp1lem7  29746  isch3  31312  nmopun  32085  2ndresdju  32722  cycpm2tr  33180  elrgspnlem1  33303  elrgspnlem2  33304  fldextrspunlsplem  33817  esumnul  34192  dya2iocnrect  34425  bnj849  35067  bnj1279  35160  cusgr3cyclex  35318  in-ax8  36406  regsfromunir1  36722  bj-0int  37413  onsucuni3  37683  wl-nfeqfb  37861  poimirlem27  37968  sticksstones20  42605  fimgmcyclem  42978  sucomisnotcard  43971  iunrelexp0  44129  frege129d  44190  clsk3nimkb  44467  gneispace  44561  eliuniin  45529  eliuniin2  45550  stoweidlem48  46476  fourierdlem42  46577  fourierdlem80  46614  eubrdm  47484  oddprmALTV  48163  grtriproplem  48415  grtrif1o  48418  pgnbgreunbgr  48601  alimp-no-surprise  50256