Theorem nexr

Inference associated with the contrapositive of 19.8a. (Contributed by Jeff Hankins, 26-Jul-2009.)

Hypothesis
nexr.1
\( \vdash \neg \exists x \, \varphi \)
Conclusion
\( \vdash \neg \varphi \)
Proof
l0
nexr.1
\( \vdash \neg \exists x \, \varphi \)
19.8a
\( \vdash \varphi \rightarrow \exists x \, \varphi \)
mto l0 _