Theorem sylbb2 228

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  ftpg  6587  wfrlem5  7589  funsnfsupp  8466  fin23lem40  9385  s4f1o  13883  fsumsplitsnun  14703  fsumsplitsnunOLD  14705  lcmcllem  15531  mat1dimbas  20500  pmatcollpw3fi  20812  nbgrssvwo2  26478  nbgrssvwo2OLD  26481  wlkn0  26747  clwlkcompbp  26909  clwlkclwwlkflem  27148  konigsberglem5  27429  eulerpartlemgs2  30772  bnj1476  31245  bnj1204  31408  dfon2lem3  32016  frrlem5  32111  bj-ccinftydisj  33429  nninfnub  33878  ispridl2  34168  rp-isfinite6  38384  fnresfnco  41730