Theorem mpisyl

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

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

Proof

Step	Hyp	Ref	Expression
1		mpisyl.1	⊢ ( 𝜑 → 𝜓 )
2		mpisyl.2	⊢ 𝜒
3		mpisyl.3	⊢ ( 𝜓 → ( 𝜒 → 𝜃 ) )
4	2 3	mpi	⊢ ( 𝜓 → 𝜃 )
5	1 4	syl	⊢ ( 𝜑 → 𝜃 )