Theorem mpisyl

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

	Ref	Expression
Hypotheses	mpisyl.1	$$⊢\phi \to \psi$$
	mpisyl.2	$$⊢\chi$$
	mpisyl.3	$$⊢\psi \to \left(\chi \to \theta \right)$$
Assertion	mpisyl	$$⊢\phi \to \theta$$

Proof

Step	Hyp	Ref	Expression
1		mpisyl.1	$$⊢\phi \to \psi$$
2		mpisyl.2	$$⊢\chi$$
3		mpisyl.3	$$⊢\psi \to \left(\chi \to \theta \right)$$
4	2 3	mpi	$$⊢\psi \to \theta$$
5	1 4	syl	$$⊢\phi \to \theta$$