Theorem ax1

Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \varphi \)
Proof
luklem5