Theorem tbw-negdf

The definition of negation, in terms of -> and \( \bot \). (Contributed by Anthony Hart, 15-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash ((\neg \varphi \rightarrow \varphi \rightarrow \bot) \rightarrow ((\varphi \rightarrow \bot) \rightarrow \neg \varphi) \rightarrow \bot) \rightarrow \bot \)
Proof
l0
pm2.21
l1
ax-1
falim
ja l1 _
pm2.43i _
l5
impbii l0 _
\( \vdash \neg \varphi \leftrightarrow \varphi \rightarrow \bot \)
tbw-bijust
\( \vdash \neg \varphi \leftrightarrow \varphi \rightarrow \bot \leftrightarrow ((\neg \varphi \rightarrow \varphi \rightarrow \bot) \rightarrow ((\varphi \rightarrow \bot) \rightarrow \neg \varphi) \rightarrow \bot) \rightarrow \bot \)
mpbi l5 _