Theorem mpisyl

Description: A syllogism combined with a modus ponens inference. (Contributed by Alan Sare, 25-Jul-2011)

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

Proof

Step	Hyp	Ref	Expression
1		mpisyl.1	|- ( ph -> ps )
2		mpisyl.2	|- ch
3		mpisyl.3	|- ( ps -> ( ch -> th ) )
4	2 3	mpi	|- ( ps -> th )
5	1 4	syl	|- ( ph -> th )