Theorem nsyli

Description: A negated syllogism inference. (Contributed by NM, 3-May-1994)

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

Proof

Step	Hyp	Ref	Expression
1		nsyli.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
2		nsyli.2	$$⊢\theta \to \neg \chi$$
3	1	con3d	$$⊢\phi \to \left(\neg \chi \to \neg \psi \right)$$
4	2 3	syl5	$$⊢\phi \to \left(\theta \to \neg \psi \right)$$