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  3673  ssdifim  4273  ralf0  4514  disjxiun  5140  wefrc  5679  frsn  5773  ssrel  5792  ssrelOLD  5793  funiun  7167  funopsn  7168  ssfi  9213  enfii  9226  nneneq  9246  fissuni  9397  inf3lem2  9669  rankvalb  9837  djur  9959  xrrebnd  13210  xaddf  13266  elfznelfzob  13812  fsuppmapnn0ub  14036  hashinfxadd  14424  hashfun  14476  fz1f1o  15746  dvdszzq  16758  clatl  18553  sgrp2nmndlem5  18942  mat1dimelbas  22477  cfinfil  23901  dyadmax  25633  ausgrusgri  29185  nbupgrres  29381  usgredgsscusgredg  29477  1egrvtxdg0  29529  wlkp1lem7  29697  isch3  31260  nmopun  32033  2ndresdju  32659  cycpm2tr  33139  elrgspnlem1  33246  elrgspnlem2  33247  fldextrspunlsplem  33723  esumnul  34049  dya2iocnrect  34283  bnj849  34939  bnj1279  35032  cusgr3cyclex  35141  in-ax8  36225  bj-0int  37102  onsucuni3  37368  wl-nfeqfb  37537  poimirlem27  37654  sticksstones20  42167  fimgmcyclem  42543  sucomisnotcard  43557  iunrelexp0  43715  frege129d  43776  clsk3nimkb  44053  gneispace  44147  eliuniin  45104  eliuniin2  45125  stoweidlem48  46063  fourierdlem42  46164  fourierdlem80  46201  eubrdm  47048  oddprmALTV  47674  grtriproplem  47906  grtrif1o  47909  alimp-no-surprise  49300