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  4649  ftpg  7095  frrlem13  8234  brinxper  8657  sdom0  9029  funsnfsupp  9283  sucprcreg  9497  fin23lem40  10249  ffz0iswrd  14450  s4f1o  14827  fsumsplitsnun  15664  lcmcllem  16509  catcone0  17595  lidldvgen  21273  mat1dimbas  22388  pmatcollpw3fi  22701  nbgrssvwo2  29342  wlkn0  29601  clwlkcompbp  29762  clwlkclwwlkflem  29986  konigsberglem5  30238  difininv  32499  prmidl2  33413  eulerpartlemgs2  34414  bnj1476  34880  bnj1204  35045  dfon2lem3  35848  bj-ccinftydisj  37278  nninfnub  37811  ispridl2  38098  rp-isfinite6  43635  fnresfnco  47165