The shortest single axiom for implicational calculus, due to Lukasiewicz.
It is now known to be the unique shortest axiom. The axiom is proved
here starting from { [ax-1], [ax-2] and peirce }. (Contributed by
Larry Lesyna and Jeffrey P. Machado, 18-Jul-2023.)
(Proof modification is discouraged.) (New usage is discouraged.)
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow (\chi \rightarrow \varphi) \rightarrow \theta \rightarrow \varphi \)
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow (\chi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \)
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \theta \rightarrow \varphi \)