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  3672  ssdifim  4278  ralf0  4519  disjxiun  5144  wefrc  5682  frsn  5775  ssrel  5794  ssrelOLD  5795  funiun  7166  funopsn  7167  ssfi  9211  enfii  9223  nneneq  9243  fissuni  9394  inf3lem2  9666  rankvalb  9834  djur  9956  xrrebnd  13206  xaddf  13262  elfznelfzob  13808  fsuppmapnn0ub  14032  hashinfxadd  14420  hashfun  14472  fz1f1o  15742  dvdszzq  16754  clatl  18565  sgrp2nmndlem5  18954  mat1dimelbas  22492  cfinfil  23916  dyadmax  25646  ausgrusgri  29199  nbupgrres  29395  usgredgsscusgredg  29491  1egrvtxdg0  29543  wlkp1lem7  29711  isch3  31269  nmopun  32042  2ndresdju  32665  cycpm2tr  33121  elrgspnlem1  33231  elrgspnlem2  33232  esumnul  34028  dya2iocnrect  34262  bnj849  34917  bnj1279  35010  cusgr3cyclex  35120  in-ax8  36206  bj-0int  37083  onsucuni3  37349  wl-nfeqfb  37516  poimirlem27  37633  sticksstones20  42147  fimgmcyclem  42519  sucomisnotcard  43533  iunrelexp0  43691  frege129d  43752  clsk3nimkb  44029  gneispace  44123  eliuniin  45038  eliuniin2  45059  stoweidlem48  46003  fourierdlem42  46104  fourierdlem80  46141  eubrdm  46985  oddprmALTV  47611  grtriproplem  47843  grtrif1o  47846  alimp-no-surprise  49011