Theorem re1luk2
luk-2 derived from the Tarski-Bernays-Wajsberg axioms. (Contributed by
Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash (\neg \varphi \rightarrow \varphi) \rightarrow \varphi \)
Proof
l0
tbw-negdf
\( \vdash ((\neg \varphi \rightarrow \varphi \rightarrow \bot) \rightarrow ((\varphi \rightarrow \bot) \rightarrow \neg \varphi) \rightarrow \bot) \rightarrow \bot \)
l1
tbw-ax2
\( \vdash (((\varphi \rightarrow \bot) \rightarrow \neg \varphi) \rightarrow \bot) \rightarrow (\neg \varphi \rightarrow \varphi \rightarrow \bot) \rightarrow ((\varphi \rightarrow \bot) \rightarrow \neg \varphi) \rightarrow \bot \)
tbwlem4
\( \vdash ((((\varphi \rightarrow \bot) \rightarrow \neg \varphi) \rightarrow \bot) \rightarrow (\neg \varphi \rightarrow \varphi \rightarrow \bot) \rightarrow ((\varphi \rightarrow \bot) \rightarrow \neg \varphi) \rightarrow \bot) \rightarrow (((\neg \varphi \rightarrow \varphi \rightarrow \bot) \rightarrow ((\varphi \rightarrow \bot) \rightarrow \neg \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow (\varphi \rightarrow \bot) \rightarrow \neg \varphi \)
ax-mp l1 _
\( \vdash (((\neg \varphi \rightarrow \varphi \rightarrow \bot) \rightarrow ((\varphi \rightarrow \bot) \rightarrow \neg \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow (\varphi \rightarrow \bot) \rightarrow \neg \varphi \)
l4
ax-mp l0 _
\( \vdash (\varphi \rightarrow \bot) \rightarrow \neg \varphi \)
tbw-ax1
\( \vdash ((\varphi \rightarrow \bot) \rightarrow \neg \varphi) \rightarrow (\neg \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \bot) \rightarrow \varphi \)
l6
ax-mp l4 _
\( \vdash (\neg \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \bot) \rightarrow \varphi \)
tbw-ax3
\( \vdash ((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi \)
tbwsyl l6 _