Theorem notnoti

Inference associated with notnot. (Contributed by NM, 27-Feb-2008.)

Hypothesis
notnoti.1
\( \vdash \varphi \)
Conclusion
\( \vdash \neg \neg \varphi \)
Proof
l0
notnoti.1
\( \vdash \varphi \)
notnot
\( \vdash \varphi \rightarrow \neg \neg \varphi \)
ax-mp l0 _