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  4698  ftpg  7148  frrlem13  8277  wfrlem5OLD  8307  sdom0  9103  funsnfsupp  9382  sucprcreg  9591  fin23lem40  10341  ffz0iswrd  14486  s4f1o  14864  fsumsplitsnun  15696  lcmcllem  16528  catcone0  17626  lidldvgen  20879  mat1dimbas  21955  pmatcollpw3fi  22268  nbgrssvwo2  28598  wlkn0  28857  clwlkcompbp  29018  clwlkclwwlkflem  29236  konigsberglem5  29488  difininv  31732  prmidl2  32516  eulerpartlemgs2  33316  bnj1476  33795  bnj1204  33960  dfon2lem3  34694  bj-ccinftydisj  36031  nninfnub  36556  ispridl2  36843  rp-isfinite6  42201  fnresfnco  45685