Theorem sylbb2 227

Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.)

Hypotheses

Ref	Expression
sylbb2.1	⊢ (𝜑 ↔ 𝜓)
sylbb2.2	⊢ (𝜒 ↔ 𝜓)

Assertion

Ref	Expression
sylbb2	⊢ (𝜑 → 𝜒)

Proof of Theorem sylbb2

Step	Hyp	Ref	Expression
1		sylbb2.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		sylbb2.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	2	biimpri 217	. 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:  ftpg  6328  wfrlem5  7306  funsnfsupp  8182  fin23lem40  9056  s4f1o  13513  fsumsplitsnun  14328  lcmcllem  15147  mat1dimbas  20097  pmatcollpw3fi  20409  usgrarnedg  25913  nbgrassvwo  25966  nbgrassvwo2  25967  nbcusgra  25992  wwlknndef  26265  clwwlknndef  26301  eulerpartlemgs2  29769  bnj1476  30171  bnj1204  30334  dfon2lem3  30934  frrlem5  31028  bj-ccinftydisj  32277  nninfnub  32717  ispridl2  33007  rp-isfinite6  36883  fnresfnco  39855  nbgrssvwo2  40587  1wlkn0  40825  konigsberglem5  41426