Theorem notnotrd

Deduction associated with notnotr and notnotri. Double negation elimination rule. A translation of the natural deduction rule -. -. C , _G |- -. -. ps => _G |- ps; see [natded]. This is Definition NNC in [Pfenning] p. 17. This rule is valid in classical logic (our logic), but not in intuitionistic logic. (Contributed by DAW, 8-Feb-2017.)

Hypothesis
notnotrd.1
\( \vdash \varphi \rightarrow \neg \neg \psi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
l0
notnotrd.1
\( \vdash \varphi \rightarrow \neg \neg \psi \)
notnotr
\( \vdash \neg \neg \psi \rightarrow \psi \)
syl l0 _