Theorem sylbb2 237

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  rexprg  4662  ftpg  7107  frrlem13  8234  wfrlem5OLD  8264  sdom0  9059  funsnfsupp  9338  sucprcreg  9546  fin23lem40  10296  ffz0iswrd  14441  s4f1o  14819  fsumsplitsnun  15651  lcmcllem  16483  catcone0  17581  lidldvgen  20784  mat1dimbas  21858  pmatcollpw3fi  22171  nbgrssvwo2  28373  wlkn0  28632  clwlkcompbp  28793  clwlkclwwlkflem  29011  konigsberglem5  29263  difininv  31508  prmidl2  32289  eulerpartlemgs2  33069  bnj1476  33548  bnj1204  33713  dfon2lem3  34446  bj-ccinftydisj  35757  nninfnub  36283  ispridl2  36570  rp-isfinite6  41912  fnresfnco  45395