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:  rexprg  4588  ftpg  6931  wfrlem5  7991  funsnfsupp  8933  sucprcreg  9141  fin23lem40  9854  ffz0iswrd  13985  s4f1o  14372  fsumsplitsnun  15206  lcmcllem  16040  catcone0  17064  lidldvgen  20150  mat1dimbas  21226  pmatcollpw3fi  21539  nbgrssvwo2  27307  wlkn0  27565  clwlkcompbp  27726  clwlkclwwlkflem  27944  konigsberglem5  28196  difininv  30441  prmidl2  31191  eulerpartlemgs2  31920  bnj1476  32401  bnj1204  32566  dfon2lem3  33338  frrlem13  33458  bj-ccinftydisj  35028  nninfnub  35555  ispridl2  35842  rp-isfinite6  40702  fnresfnco  44097