I’ve been self-studying axiomatic systems for classical logic for a while. The standard Hilbert/Mendelssohn/Lukasiewicz axiomatizations were a bit tough for me to get used to without using the Deduction Theorem, but now I’m confident with those systems.


I recently learned about Meredith’s axiom for classical logic:


$((((A \to B) \to (\neg C \to \neg D)) \to C) \to E) \to (E \to A) \to D \to A$.


Could anyone give me tips for constructing proofs in this system? It seems obvious that one just needs to find the correct substitution of an instance of the axiom into the antecedent of another instance of the axiom, but I can’t seem to get any further than that strategy. Any help would be appreciated.



How to use Meredith’s axiom for classical logic?
See <https://us.metamath.org/mpeuni/meredith.html> and the links there for the proofs you want.


