Theorem luklem3

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