Theorem luklem2

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 \neg \psi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \theta) \rightarrow \psi \rightarrow \theta \)
Proof
l0
luk-1
\( \vdash (\varphi \rightarrow \neg \psi) \rightarrow (\neg \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l1
luk-3
\( \vdash \psi \rightarrow \neg \psi \rightarrow \chi \)
luk-1
\( \vdash (\psi \rightarrow \neg \psi \rightarrow \chi) \rightarrow ((\neg \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
ax-mp l1 _
\( \vdash ((\neg \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
l4
luklem1 l0 _
\( \vdash (\varphi \rightarrow \neg \psi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
luk-1
\( \vdash (\psi \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \theta) \rightarrow \psi \rightarrow \theta \)
luklem1 l4 _