Theorem sylbb 211

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  bitri  267  ssdifim  4063  disjxiun  4840  trintOLD  4962  pocl  5240  wefrc  5306  frsn  5394  ssrel  5412  funiun  6640  funopsn  6641  fissuni  8513  inf3lem2  8776  rankvalb  8910  djur  9031  xrrebnd  12248  xaddf  12304  elfznelfzob  12829  fsuppmapnn0ub  13049  hashinfxadd  13424  hashfun  13473  fz1f1o  14782  clatl  17431  sgrp2nmndlem5  17732  mat1dimelbas  20603  cfinfil  22025  dyadmax  23706  ausgrusgri  26404  nbupgrres  26607  usgredgsscusgredg  26709  1egrvtxdg0  26761  wlkp1lem7  26932  wwlksnfi  27186  isch3  28623  nmopun  29398  esumnul  30626  dya2iocnrect  30859  bnj849  31512  bnj1279  31603  bj-0int  33548  onsucuni3  33713  wl-nfeqfb  33813  poimirlem27  33925  unitresl  34371  iunrelexp0  38773  frege129d  38834  clsk3nimkb  39116  gneispace  39210  eliuniin  40034  eliuniin2  40057  stoweidlem48  41004  fourierdlem42  41105  fourierdlem80  41142  eubrdm  41915  oddprmALTV  42376  alimp-no-surprise  43325