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  3640  ssdifim  4236  ralf0  4477  disjxiun  5104  wefrc  5632  frsn  5726  ssrel  5745  ssrelOLD  5746  funiun  7119  funopsn  7120  ssfi  9137  enfii  9150  nneneq  9170  fissuni  9308  inf3lem2  9582  rankvalb  9750  djur  9872  xrrebnd  13128  xaddf  13184  elfznelfzob  13734  fsuppmapnn0ub  13960  hashinfxadd  14350  hashfun  14402  fz1f1o  15676  dvdszzq  16691  clatl  18467  sgrp2nmndlem5  18856  mat1dimelbas  22358  cfinfil  23780  dyadmax  25499  ausgrusgri  29095  nbupgrres  29291  usgredgsscusgredg  29387  1egrvtxdg0  29439  wlkp1lem7  29607  isch3  31170  nmopun  31943  2ndresdju  32573  cycpm2tr  33076  elrgspnlem1  33193  elrgspnlem2  33194  fldextrspunlsplem  33668  esumnul  34038  dya2iocnrect  34272  bnj849  34915  bnj1279  35008  cusgr3cyclex  35123  in-ax8  36212  bj-0int  37089  onsucuni3  37355  wl-nfeqfb  37524  poimirlem27  37641  sticksstones20  42154  fimgmcyclem  42521  sucomisnotcard  43533  iunrelexp0  43691  frege129d  43752  clsk3nimkb  44029  gneispace  44123  eliuniin  45093  eliuniin2  45114  stoweidlem48  46046  fourierdlem42  46147  fourierdlem80  46184  eubrdm  47037  oddprmALTV  47688  grtriproplem  47938  grtrif1o  47941  pgnbgreunbgr  48115  alimp-no-surprise  49770