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  4651  ftpg  7094  frrlem13  8238  brinxper  8661  sdom0  9033  funsnfsupp  9301  sucprcreg  9515  fin23lem40  10264  ffz0iswrd  14466  s4f1o  14843  fsumsplitsnun  15680  lcmcllem  16525  catcone0  17611  lidldvgen  21259  mat1dimbas  22375  pmatcollpw3fi  22688  nbgrssvwo2  29325  wlkn0  29584  clwlkcompbp  29745  clwlkclwwlkflem  29966  konigsberglem5  30218  difininv  32479  prmidl2  33388  eulerpartlemgs2  34347  bnj1476  34813  bnj1204  34978  dfon2lem3  35758  bj-ccinftydisj  37186  nninfnub  37730  ispridl2  38017  rp-isfinite6  43491  fnresfnco  47026