Theorem luklem1

Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 23-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
luklem1.1
\( \vdash \varphi \rightarrow \psi \)
luklem1.2
\( \vdash \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
l0
luklem1.2
\( \vdash \psi \rightarrow \chi \)
l1
luklem1.1
\( \vdash \varphi \rightarrow \psi \)
luk-1
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l1 _
\( \vdash (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l0 _