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  4702  ftpg  7176  frrlem13  8322  wfrlem5OLD  8352  brinxper  8773  sdom0  9147  funsnfsupp  9430  sucprcreg  9639  fin23lem40  10389  ffz0iswrd  14576  s4f1o  14954  fsumsplitsnun  15788  lcmcllem  16630  catcone0  17732  lidldvgen  21362  mat1dimbas  22494  pmatcollpw3fi  22807  nbgrssvwo2  29394  wlkn0  29654  clwlkcompbp  29815  clwlkclwwlkflem  30033  konigsberglem5  30285  difininv  32545  prmidl2  33449  eulerpartlemgs2  34362  bnj1476  34840  bnj1204  35005  dfon2lem3  35767  bj-ccinftydisj  37196  nninfnub  37738  ispridl2  38025  rp-isfinite6  43508  fnresfnco  46991