Theorem ax2

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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
Proof
l0
luklem7
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
l1
luklem8
\( \vdash (\psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \varphi \rightarrow \chi \)
l2
luklem6
\( \vdash (\varphi \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
luklem8
\( \vdash ((\varphi \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l2 _
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
luklem1 l1 _
\( \vdash (\psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
luklem1 l0 _