Theorem syl6mpi

Description: A syllogism inference. (Contributed by Alan Sare, 8-Jul-2011) (Proof shortened by Wolf Lammen, 13-Sep-2012)

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

Proof

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