Theorem luk-3

3 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \varphi \rightarrow \neg \varphi \rightarrow \psi \)
Proof
l0
merlem11
\( \vdash (\neg \varphi \rightarrow \neg \varphi \rightarrow \psi) \rightarrow \neg \varphi \rightarrow \psi \)
merlem1
\( \vdash ((\neg \varphi \rightarrow \neg \varphi \rightarrow \psi) \rightarrow \neg \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \neg \varphi \rightarrow \psi \)
ax-mp l0 _