Theorem sylbb 208

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  bitri  263  disjxiun  4579  trint  4696  pocl  4966  wefrc  5032  frsn  5112  ssrel  5130  funiun  6318  funopsn  6319  fissuni  8154  inf3lem2  8409  rankvalb  8543  xrrebnd  11873  xaddf  11929  elfznelfzob  12440  fsuppmapnn0ub  12657  hashinfxadd  13035  hashfun  13084  clatl  16939  sgrp2nmndlem5  17239  mat1dimelbas  20096  cfinfil  21507  dyadmax  23172  wwlknfi  26266  isch3  27482  nmopun  28257  esumnul  29437  dya2iocnrect  29670  bnj849  30249  bnj1279  30340  onsucuni3  32391  wl-nfeqfb  32502  poimirlem27  32606  unitresl  33054  iunrelexp0  37013  frege129d  37074  clsk3nimkb  37358  gneispace  37452  stoweidlem48  38941  fourierdlem42  39042  fourierdlem80  39079  oddprmALTV  40136  ausgrusgri  40398  nbupgrres  40592  usgredgsscusgredg  40675  1egrvtxdg0  40727  1wlkp1lem7  40888  wwlksnfi  41112  alimp-no-surprise  42336