Theorem ax3

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

Conclusion
\( \vdash (\neg \varphi \rightarrow \neg \psi) \rightarrow \psi \rightarrow \varphi \)
Proof
l0
luklem2
\( \vdash (\neg \varphi \rightarrow \neg \psi) \rightarrow ((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi \)
luklem4
\( \vdash (((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi \)
luklem1 l0 _