Theorem luklem5

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 \varphi \)
Proof
l0
luklem3
\( \vdash \varphi \rightarrow ((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi \)
luklem4
\( \vdash (((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi \)
luklem1 l0 _