Theorem nsyli

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

	Ref	Expression
Hypotheses	nsyli.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
	nsyli.2	⊢ ( 𝜃 → ¬ 𝜒 )
Assertion	nsyli	⊢ ( 𝜑 → ( 𝜃 → ¬ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		nsyli.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2		nsyli.2	⊢ ( 𝜃 → ¬ 𝜒 )
3	1	con3d	⊢ ( 𝜑 → ( ¬ 𝜒 → ¬ 𝜓 ) )
4	2 3	syl5	⊢ ( 𝜑 → ( 𝜃 → ¬ 𝜓 ) )