Theorem sylancl

Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypotheses	sylancl.1	⊢ ( 𝜑 → 𝜓 )
	sylancl.2	⊢ 𝜒
	sylancl.3	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
Assertion	sylancl	⊢ ( 𝜑 → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		sylancl.1	⊢ ( 𝜑 → 𝜓 )
2		sylancl.2	⊢ 𝜒
3		sylancl.3	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
4	2	a1i	⊢ ( 𝜑 → 𝜒 )
5	1 4 3	syl2anc	⊢ ( 𝜑 → 𝜃 )