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  4701  ftpg  7154  frrlem13  8283  wfrlem5OLD  8313  sdom0  9108  funsnfsupp  9387  sucprcreg  9596  fin23lem40  10346  ffz0iswrd  14491  s4f1o  14869  fsumsplitsnun  15701  lcmcllem  16533  catcone0  17631  lidldvgen  20893  mat1dimbas  21974  pmatcollpw3fi  22287  nbgrssvwo2  28619  wlkn0  28878  clwlkcompbp  29039  clwlkclwwlkflem  29257  konigsberglem5  29509  difininv  31755  prmidl2  32559  eulerpartlemgs2  33379  bnj1476  33858  bnj1204  34023  dfon2lem3  34757  bj-ccinftydisj  36094  nninfnub  36619  ispridl2  36906  rp-isfinite6  42269  fnresfnco  45751