Theorem fal

The truth value \( \bot \) is refutable. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Mel L. O'Cat, 11-Mar-2012.)

Conclusion
\( \vdash \neg \bot \)
Proof
tru
l1
notnoti _
\( \vdash \neg \neg \top \)
df-fal
\( \vdash \bot \leftrightarrow \neg \top \)
mtbir l1 _