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  4656  ftpg  7111  frrlem13  8250  brinxper  8675  sdom0  9049  funsnfsupp  9307  sucprcreg  9521  fin23lem40  10273  ffz0iswrd  14476  s4f1o  14853  fsumsplitsnun  15690  lcmcllem  16535  catcone0  17622  lidldvgen  21301  mat1dimbas  22428  pmatcollpw3fi  22741  nbgrssvwo2  29447  wlkn0  29706  clwlkcompbp  29867  clwlkclwwlkflem  30091  konigsberglem5  30343  difininv  32603  prmidl2  33533  eulerpartlemgs2  34557  bnj1476  35022  bnj1204  35187  noinfepregs  35308  dfon2lem3  35996  bj-ccinftydisj  37462  nninfnub  37996  ispridl2  38283  rp-isfinite6  43868  fnresfnco  47395