Theorem notnotri

Inference associated with notnotr. For a shorter proof using [ax-2], see notnotriALT. (Contributed by NM, 27-Feb-2008.) (Proof shortened by Wolf Lammen, 15-Jul-2021.) Remove dependency on [ax-2]. (Revised by Steven Nguyen, 27-Dec-2022.)

Hypothesis
notnotri.1
\( \vdash \neg \neg \varphi \)
Conclusion
\( \vdash \varphi \)
Proof
l0
notnotri.1
\( \vdash \neg \neg \varphi \)
notnotri.1
pm2.21i _
\( \vdash \neg \varphi \rightarrow \neg \neg \neg \varphi \)
mt4 l0 _