Theorem mpsylsyld

Description: Modus ponens combined with a double syllogism inference. (Contributed by Alan Sare, 22-Jul-2012)

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

Proof

Step	Hyp	Ref	Expression
1		mpsylsyld.1	$$⊢\phi$$
2		mpsylsyld.2	$$⊢\psi \to \left(\chi \to \theta \right)$$
3		mpsylsyld.3	$$⊢\phi \to \left(\theta \to \tau \right)$$
4	1	a1i	$$⊢\psi \to \phi$$
5	4 2 3	sylsyld	$$⊢\psi \to \left(\chi \to \tau \right)$$