Theorem sylbb 222

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bitri  278  unitreslOLD  875  ssdifim  4189  disjxiun  5027  pocl  5445  wefrc  5513  frsn  5603  ssrel  5621  funiun  6886  funopsn  6887  fissuni  8813  inf3lem2  9076  rankvalb  9210  djur  9332  xrrebnd  12549  xaddf  12605  elfznelfzob  13138  fsuppmapnn0ub  13358  hashinfxadd  13742  hashfun  13794  fz1f1o  15059  clatl  17718  sgrp2nmndlem5  18086  mat1dimelbas  21076  cfinfil  22498  dyadmax  24202  ausgrusgri  26961  nbupgrres  27154  usgredgsscusgredg  27249  1egrvtxdg0  27301  wlkp1lem7  27469  isch3  29024  nmopun  29797  2ndresdju  30411  dvdszzq  30557  cycpm2tr  30811  esumnul  31417  dya2iocnrect  31649  bnj849  32307  bnj1279  32400  cusgr3cyclex  32496  bj-0int  34516  onsucuni3  34784  wl-nfeqfb  34941  poimirlem27  35084  iunrelexp0  40403  frege129d  40464  clsk3nimkb  40743  gneispace  40837  eliuniin  41735  eliuniin2  41755  stoweidlem48  42690  fourierdlem42  42791  fourierdlem80  42828  eubrdm  43628  oddprmALTV  44205  alimp-no-surprise  45309