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	$$⊢\phi \to \psi$$
	mpnanrd.2	$$⊢\phi \to \neg \left(\psi \wedge \chi \right)$$
Assertion	mpnanrd	$$⊢\phi \to \neg \chi$$

Proof

Step	Hyp	Ref	Expression
1		mpnanrd.1	$$⊢\phi \to \psi$$
2		mpnanrd.2	$$⊢\phi \to \neg \left(\psi \wedge \chi \right)$$
3		imnan	$$⊢\left(\psi \to \neg \chi \right)\leftrightarrow \neg \left(\psi \wedge \chi \right)$$
4	2 3	sylibr	$$⊢\phi \to \left(\psi \to \neg \chi \right)$$
5	1 4	mpd	$$⊢\phi \to \neg \chi$$