Theorem sylbb2 238

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  rexprg  4661  ftpg  7128  frrlem13  8277  brinxper  8700  sdom0  9073  funsnfsupp  9343  sucprcreg  9554  fin23lem40  10304  ffz0iswrd  14506  s4f1o  14884  fsumsplitsnun  15721  lcmcllem  16566  catcone0  17648  lidldvgen  21244  mat1dimbas  22359  pmatcollpw3fi  22672  nbgrssvwo2  29289  wlkn0  29549  clwlkcompbp  29712  clwlkclwwlkflem  29933  konigsberglem5  30185  difininv  32446  prmidl2  33412  eulerpartlemgs2  34371  bnj1476  34837  bnj1204  35002  dfon2lem3  35773  bj-ccinftydisj  37201  nninfnub  37745  ispridl2  38032  rp-isfinite6  43507  fnresfnco  47042