Theorem nexdh

Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.)

Hypotheses
nexdh.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
nexdh.2
\( \vdash \varphi \rightarrow \neg \psi \)
Conclusion
\( \vdash \varphi \rightarrow \neg \exists x \, \psi \)
Proof
l0
nexdh.1
nexdh.2
l2
alrimih l0 _
\( \vdash \varphi \rightarrow \forall x \, \neg \psi \)
alnex
\( \vdash \forall x \, \neg \psi \leftrightarrow \neg \exists x \, \psi \)
sylib l2 _