Theorem merco2

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

This axiom has 19 symbols, sans auxiliaries. See notes in merco1. (Contributed by Anthony Hart, 7-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash ((\varphi \rightarrow \psi) \rightarrow (\bot \rightarrow \chi) \rightarrow \theta) \rightarrow (\theta \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi \)
Proof
l0
falim
\( \vdash \bot \rightarrow \chi \)
pm2.04
\( \vdash ((\varphi \rightarrow \psi) \rightarrow (\bot \rightarrow \chi) \rightarrow \theta) \rightarrow (\bot \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \theta \)
l2
mpi l0 _
\( \vdash ((\varphi \rightarrow \psi) \rightarrow (\bot \rightarrow \chi) \rightarrow \theta) \rightarrow (\varphi \rightarrow \psi) \rightarrow \theta \)
l3
jarl
idd
l5
jad l3 _
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \theta) \rightarrow (\varphi \rightarrow \theta) \rightarrow \theta \)
looinv
\( \vdash ((\varphi \rightarrow \theta) \rightarrow \theta) \rightarrow (\theta \rightarrow \varphi) \rightarrow \varphi \)
3syl l2 l5 _
a1dd _
a1i _
com4l _