Theorem tbwlem2
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 ((\varphi \rightarrow \chi) \rightarrow \theta) \rightarrow \psi \rightarrow \theta \)
Proof
l0
tbw-ax1
\( \vdash (\varphi \rightarrow \psi \rightarrow \bot) \rightarrow ((\psi \rightarrow \bot) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l1
tbw-ax4
\( \vdash \bot \rightarrow \chi \)
l2
tbw-ax1
\( \vdash (\psi \rightarrow \bot) \rightarrow (\bot \rightarrow \chi) \rightarrow \psi \rightarrow \chi \)
tbwlem1
\( \vdash ((\psi \rightarrow \bot) \rightarrow (\bot \rightarrow \chi) \rightarrow \psi \rightarrow \chi) \rightarrow (\bot \rightarrow \chi) \rightarrow (\psi \rightarrow \bot) \rightarrow \psi \rightarrow \chi \)
ax-mp l2 _
\( \vdash (\bot \rightarrow \chi) \rightarrow (\psi \rightarrow \bot) \rightarrow \psi \rightarrow \chi \)
l5
ax-mp l1 _
\( \vdash (\psi \rightarrow \bot) \rightarrow \psi \rightarrow \chi \)
tbwlem1
\( \vdash ((\psi \rightarrow \bot) \rightarrow \psi \rightarrow \chi) \rightarrow \psi \rightarrow (\psi \rightarrow \bot) \rightarrow \chi \)
l7
ax-mp l5 _
\( \vdash \psi \rightarrow (\psi \rightarrow \bot) \rightarrow \chi \)
tbw-ax1
\( \vdash (\psi \rightarrow (\psi \rightarrow \bot) \rightarrow \chi) \rightarrow (((\psi \rightarrow \bot) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
ax-mp l7 _
\( \vdash (((\psi \rightarrow \bot) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
l10
tbwsyl l0 _
\( \vdash (\varphi \rightarrow \psi \rightarrow \bot) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
tbw-ax1
\( \vdash (\psi \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \theta) \rightarrow \psi \rightarrow \theta \)
tbwsyl l10 _