Theorem sylbb2 241

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  ftpg  6895  wfrlem5  7942  funsnfsupp  8841  sucprcreg  9049  fin23lem40  9762  ffz0iswrd  13884  s4f1o  14271  fsumsplitsnun  15102  lcmcllem  15930  lidldvgen  20021  mat1dimbas  21077  pmatcollpw3fi  21390  nbgrssvwo2  27152  wlkn0  27410  clwlkcompbp  27571  clwlkclwwlkflem  27789  konigsberglem5  28041  difininv  30288  prmidl2  31024  eulerpartlemgs2  31748  bnj1476  32229  bnj1204  32394  dfon2lem3  33143  frrlem13  33248  bj-ccinftydisj  34628  nninfnub  35189  ispridl2  35476  rp-isfinite6  40226  fnresfnco  43633