Theorem mpnanrd

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

Hypotheses
mpnanrd.1
\( \vdash \varphi \rightarrow \psi \)
mpnanrd.2
\( \vdash \varphi \rightarrow \neg (\psi \wedge \chi) \)
Conclusion
\( \vdash \varphi \rightarrow \neg \chi \)
Proof
l0
mpnanrd.1
\( \vdash \varphi \rightarrow \psi \)
l1
mpnanrd.2
\( \vdash \varphi \rightarrow \neg (\psi \wedge \chi) \)
imnan
\( \vdash \psi \rightarrow \neg \chi \leftrightarrow \neg (\psi \wedge \chi) \)
sylibr l1 _
\( \vdash \varphi \rightarrow \psi \rightarrow \neg \chi \)
mpd l0 _