Theorem luklem6
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 \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
Proof
l0
luk-1
\( \vdash (\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
l1
luklem5
\( \vdash \neg (\varphi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg (\varphi \rightarrow \psi) \)
l2
luklem2
\( \vdash (\neg \psi \rightarrow \neg (\varphi \rightarrow \psi)) \rightarrow ((\neg \psi \rightarrow \psi) \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \psi \)
luklem4
\( \vdash (((\neg \psi \rightarrow \psi) \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \psi \)
luklem1 l2 _
\( \vdash (\neg \psi \rightarrow \neg (\varphi \rightarrow \psi)) \rightarrow (\varphi \rightarrow \psi) \rightarrow \psi \)
l5
luklem1 l1 _
\( \vdash \neg (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \psi \)
luk-1
\( \vdash (\neg (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow \neg (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
l7
ax-mp l5 _
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow \neg (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
luk-1
\( \vdash ((((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow \neg (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\neg (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
l9
ax-mp l7 _
\( \vdash ((\neg (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
luklem4
\( \vdash (((\neg (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
ax-mp l9 _
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
luklem1 l0 _