Theorem syl6ci

Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 18-Mar-2012)

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

Proof

Step	Hyp	Ref	Expression
1		syl6ci.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
2		syl6ci.2	$$⊢\phi \to \theta$$
3		syl6ci.3	$$⊢\chi \to \left(\theta \to \tau \right)$$
4	2	a1d	$$⊢\phi \to \left(\psi \to \theta \right)$$
5	1 4 3	syl6c	$$⊢\phi \to \left(\psi \to \tau \right)$$