Theorem notnotd

Deduction associated with notnot and notnoti. (Contributed by Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf Lammen, 27-Mar-2021.)

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