Theorem sylbb2 240

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  ftpg  6912  wfrlem5  7953  funsnfsupp  8851  sucprcreg  9059  fin23lem40  9767  ffz0iswrd  13885  s4f1o  14274  fsumsplitsnun  15104  lcmcllem  15934  lidldvgen  20022  mat1dimbas  21075  pmatcollpw3fi  21387  nbgrssvwo2  27138  wlkn0  27396  clwlkcompbp  27557  clwlkclwwlkflem  27776  konigsberglem5  28029  difininv  30273  prmidl2  30953  eulerpartlemgs2  31633  bnj1476  32114  bnj1204  32279  dfon2lem3  33025  frrlem13  33130  bj-ccinftydisj  34489  nninfnub  35020  ispridl2  35310  rp-isfinite6  39877  fnresfnco  43270