Theorem sylancr

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

	Ref	Expression
Hypotheses	sylancr.1	|- ps
	sylancr.2	|- ( ph -> ch )
	sylancr.3	|- ( ( ps /\ ch ) -> th )
Assertion	sylancr	|- ( ph -> th )

Proof

Step	Hyp	Ref	Expression
1		sylancr.1	|- ps
2		sylancr.2	|- ( ph -> ch )
3		sylancr.3	|- ( ( ps /\ ch ) -> th )
4	1	a1i	|- ( ph -> ps )
5	4 2 3	syl2anc	|- ( ph -> th )