Theorem sylbb2 237

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  rexprg  4629  ftpg  7010  frrlem13  8085  wfrlem5OLD  8115  funsnfsupp  9082  sucprcreg  9290  fin23lem40  10038  ffz0iswrd  14172  s4f1o  14559  fsumsplitsnun  15395  lcmcllem  16229  catcone0  17313  lidldvgen  20439  mat1dimbas  21529  pmatcollpw3fi  21842  nbgrssvwo2  27632  wlkn0  27890  clwlkcompbp  28051  clwlkclwwlkflem  28269  konigsberglem5  28521  difininv  30765  prmidl2  31518  eulerpartlemgs2  32247  bnj1476  32727  bnj1204  32892  dfon2lem3  33667  bj-ccinftydisj  35311  nninfnub  35836  ispridl2  36123  rp-isfinite6  41023  fnresfnco  44422