Theorem sylbb 221

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 218	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	sylbi 219	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bitri  277  ssdifim  4225  disjxiun  5096  wefrc  5639  frsn  5733  ssrel  5753  funiun  7125  funopsn  7126  funopsnOLD  7127  ssfi  9137  enfii  9150  nneneq  9170  fissuni  9297  inf3lem2  9581  rankvalb  9752  djur  9874  xrrebnd  13168  xaddf  13224  elfznelfzob  13777  fsuppmapnn0ub  14005  hashinfxadd  14395  hashfun  14447  fz1f1o  15720  dvdszzq  16739  clatl  18523  sgrp2nmndlem5  18949  mat1dimelbas  22511  cfinfil  23933  dyadmax  25640  ausgrusgri  29315  nbupgrres  29511  usgredgsscusgredg  29606  1egrvtxdg0  29658  wlkp1lem7  29824  isch3  31390  nmopun  32163  2ndresdju  32801  cycpm2tr  33260  elrgspnlem1  33384  elrgspnlem2  33385  fldextrspunlsplem  33931  esumnul  34306  dya2iocnrect  34539  bnj849  35184  bnj1279  35277  cusgr3cyclex  35450  in-ax8  36548  regsfromunir1  36864  bj-0int  37555  onsucuni3  37825  wl-nfeqfb  38003  poimirlem27  38110  sticksstones20  42747  fimgmcyclem  43115  sucomisnotcard  44084  iunrelexp0  44242  frege129d  44303  clsk3nimkb  44580  gneispace  44674  eliuniin  45641  eliuniin2  45662  stoweidlem48  46586  fourierdlem42  46687  fourierdlem80  46724  eubrdm  47594  oddprmALTV  48273  grtriproplem  48525  grtrif1o  48528  pgnbgreunbgr  48711  alimp-no-surprise  50366