Theorem nex

Generalization rule for negated wff. (Contributed by NM, 18-May-1994.)

Hypothesis
nex.1
\( \vdash \neg \varphi \)
Conclusion
\( \vdash \neg \exists x \, \varphi \)
Proof
l0
alnex
\( \vdash \forall x \, \neg \varphi \leftrightarrow \neg \exists x \, \varphi \)
nex.1
\( \vdash \neg \varphi \)
mpgbi l0 _