Theorem orsird

A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)

Hypothesis
orsild.1
\( \vdash \varphi \rightarrow \neg (\psi \vee \chi) \)
Conclusion
\( \vdash \varphi \rightarrow \neg \chi \)
Proof
l0
orsild.1
\( \vdash \varphi \rightarrow \neg (\psi \vee \chi) \)
ioran
\( \vdash \neg (\psi \vee \chi) \leftrightarrow \neg \psi \wedge \neg \chi \)
sylib l0 _
\( \vdash \varphi \rightarrow \neg \psi \wedge \neg \chi \)
simprd _