Theorem sylc

Description: A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994) (Revised by NM, 13-Jul-2013)

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

Proof

Step	Hyp	Ref	Expression
1		sylc.1	$$⊢\phi \to \psi$$
2		sylc.2	$$⊢\phi \to \chi$$
3		sylc.3	$$⊢\psi \to \left(\chi \to \theta \right)$$
4	1 2 3	syl2im	$$⊢\phi \to \left(\phi \to \theta \right)$$
5	4	pm2.43i	$$⊢\phi \to \theta$$