Theorem luklem7
Used to rederive standard propositional axioms from Lukasiewicz'.
(Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
Proof
l0
luk-1
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l1
luklem5
\( \vdash \psi \rightarrow (\psi \rightarrow \chi) \rightarrow \psi \)
luk-1
\( \vdash ((\psi \rightarrow \chi) \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \chi \)
l3
luklem1 l1 _
\( \vdash \psi \rightarrow (\psi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \chi \)
luklem6
\( \vdash ((\psi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \chi \)
l5
luklem1 l3 _
\( \vdash \psi \rightarrow (\psi \rightarrow \chi) \rightarrow \chi \)
luk-1
\( \vdash (\psi \rightarrow (\psi \rightarrow \chi) \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
ax-mp l5 _
\( \vdash (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
luklem1 l0 _