Theorem tbwlem3
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 \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow \psi \)
Proof
l0
tbw-ax3
\( \vdash ((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi \)
l1
tbw-ax2
\( \vdash (((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow ((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi \)
tbw-ax1
\( \vdash (((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow ((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow \psi \)
tbwsyl l1 _
\( \vdash (((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow \psi \)
l4
ax-mp l0 _
\( \vdash ((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow \psi \)
l5
tbw-ax1
\( \vdash (((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow \psi) \rightarrow ((((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow \psi) \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow \psi \)
tbw-ax3
\( \vdash (((((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow \psi) \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow \psi \)
tbwsyl l5 _
\( \vdash (((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow \psi \)
ax-mp l4 _