Theorem tbwlem5

Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash ((\varphi \rightarrow \psi \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \)
Proof
l0
tbw-ax2
\( \vdash \varphi \rightarrow \psi \rightarrow \varphi \)
tbw-ax1
\( \vdash (\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \bot) \rightarrow \psi \rightarrow \bot \)
l2
tbwsyl l0 _
\( \vdash \varphi \rightarrow (\varphi \rightarrow \bot) \rightarrow \psi \rightarrow \bot \)
tbwlem1
\( \vdash (\varphi \rightarrow (\varphi \rightarrow \bot) \rightarrow \psi \rightarrow \bot) \rightarrow (\varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \psi \rightarrow \bot \)
l4
ax-mp l2 _
\( \vdash (\varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \psi \rightarrow \bot \)
tbwlem4
\( \vdash ((\varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \psi \rightarrow \bot) \rightarrow ((\varphi \rightarrow \psi \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \)
ax-mp l4 _