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  4169  ralf0  4409  disjxiun  5032  pocl  5453  wefrc  5521  frsn  5612  ssrel  5630  funiun  6905  funopsn  6906  ssfi  8747  fissuni  8867  inf3lem2  9130  rankvalb  9264  djur  9386  xrrebnd  12607  xaddf  12663  elfznelfzob  13197  fsuppmapnn0ub  13417  hashinfxadd  13801  hashfun  13853  fz1f1o  15120  clatl  17797  sgrp2nmndlem5  18165  mat1dimelbas  21176  cfinfil  22598  dyadmax  24303  ausgrusgri  27065  nbupgrres  27258  usgredgsscusgredg  27353  1egrvtxdg0  27405  wlkp1lem7  27573  isch3  29128  nmopun  29901  2ndresdju  30513  dvdszzq  30657  cycpm2tr  30916  esumnul  31539  dya2iocnrect  31771  bnj849  32429  bnj1279  32522  cusgr3cyclex  32618  bj-0int  34822  onsucuni3  35090  wl-nfeqfb  35247  poimirlem27  35390  iunrelexp0  40804  frege129d  40865  clsk3nimkb  41144  gneispace  41238  eliuniin  42136  eliuniin2  42156  stoweidlem48  43084  fourierdlem42  43185  fourierdlem80  43222  eubrdm  44022  oddprmALTV  44600  alimp-no-surprise  45773