Theorem dfnot

Given falsum \( \bot \), we can define the negation of a wff \( \varphi \) as the statement that \( \bot \) follows from assuming \( \varphi \). (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 21-Jul-2019.)

Conclusion
\( \vdash \neg \varphi \leftrightarrow \varphi \rightarrow \bot \)
Proof
l0
fal
\( \vdash \neg \bot \)
mtt
\( \vdash \neg \bot \rightarrow (\neg \varphi \leftrightarrow \varphi \rightarrow \bot) \)
ax-mp l0 _