Theorem merco1

A single axiom for propositional calculus discovered by C. A. Meredith.

This axiom is worthy of note, due to it having only 19 symbols, not counting parentheses. The more well-known meredith has 21 symbols, sans parentheses.

See merco2 for another axiom of equal length. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash ((((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \bot) \rightarrow \theta) \rightarrow \tau) \rightarrow (\tau \rightarrow \varphi) \rightarrow \chi \rightarrow \varphi \)
Proof
l0
ax-1
falim
ja l0 _
imim2i _
imim1i _
l5
imim1i _
\( \vdash ((((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \bot) \rightarrow \theta) \rightarrow \tau) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \neg \theta \rightarrow \neg \chi) \rightarrow \theta) \rightarrow \tau \)
meredith
\( \vdash ((((\varphi \rightarrow \psi) \rightarrow \neg \theta \rightarrow \neg \chi) \rightarrow \theta) \rightarrow \tau) \rightarrow (\tau \rightarrow \varphi) \rightarrow \chi \rightarrow \varphi \)
syl l5 _