Theorem mpnanrd

Description: Eliminate the right side of a negated conjunction in an implication. (Contributed by ML, 17-Oct-2020)

	Ref	Expression
Hypotheses	mpnanrd.1	⊢ ( 𝜑 → 𝜓 )
	mpnanrd.2	⊢ ( 𝜑 → ¬ ( 𝜓 ∧ 𝜒 ) )
Assertion	mpnanrd	⊢ ( 𝜑 → ¬ 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		mpnanrd.1	⊢ ( 𝜑 → 𝜓 )
2		mpnanrd.2	⊢ ( 𝜑 → ¬ ( 𝜓 ∧ 𝜒 ) )
3		imnan	⊢ ( ( 𝜓 → ¬ 𝜒 ) ↔ ¬ ( 𝜓 ∧ 𝜒 ) )
4	2 3	sylibr	⊢ ( 𝜑 → ( 𝜓 → ¬ 𝜒 ) )
5	1 4	mpd	⊢ ( 𝜑 → ¬ 𝜒 )