Theorem pm3.2ni

Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.)

Hypotheses
pm3.2ni.1
\( \vdash \neg \varphi \)
pm3.2ni.2
\( \vdash \neg \psi \)
Conclusion
\( \vdash \neg (\varphi \vee \psi) \)
Proof
l0
pm3.2ni.1
\( \vdash \neg \varphi \)
l1
id
pm3.2ni.2
pm2.21i _
jaoi l1 _
\( \vdash \varphi \vee \psi \rightarrow \varphi \)
mto l0 _