Proving law of excluded middle and double negation elimination are equivalent

Question

I'm self-studying propositional calculus, and one of the exercises is to prove that replacing the law of excluded middle ($A \lor \lnot A$) with double negation elimination (that is, $\lnot \lnot A \rightarrow A$) does not change the set of provable theorems in the axiomatic set.

The most obvious way to prove this is to prove the claim in the title. I managed to prove it in one direction, that is $A \lor \lnot A$ along with other schemas implies $\lnot \lnot A \rightarrow A$, but I'm quite stuck with the other direction.

So, the ten remaining axiom schemas (after removing the law of excluded middle) are as follows:

1. $A \rightarrow (B \rightarrow A)$;
2. $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$;
3. $(A \land B) \rightarrow A$;
4. $(A \land B) \rightarrow B$;
5. $A \rightarrow (B \rightarrow (A \land B))$;
6. $A \rightarrow (A \lor B)$;
7. $B \rightarrow (A \lor B)$;
8. $(A \rightarrow C) \rightarrow ((B \rightarrow C) \rightarrow (A \lor B \rightarrow C))$;
9. $\lnot A \rightarrow (A \rightarrow B)$;
10. $(A \rightarrow B) \rightarrow ((A \rightarrow \lnot B) \rightarrow \lnot A)$.

I'm only having modus ponens as the inference rule, and I'm not supposed to know about $\bot$ yet (since some similar questions here mention it).

I also managed to prove $\lnot \lnot \lnot A \rightarrow \lnot A$ and $A \rightarrow \lnot \lnot A$ in the meanwhile, but they don't seem to help here.

Answer 1

Hint

1) $\lnot (A \lor \lnot A)$ --- premise

2) $\vdash A \to (A \lor \lnot A)$ --- axiom Ax.6

3) $A \to \lnot (A \lor \lnot A)$ --- axiom Ax.1 and 1) by mp

4) $\lnot A$ --- 2) and 3) and axiom Ax.10 by mp twice

5) $\vdash \lnot A \to (A \lor \lnot A)$ --- axiom Ax.7

6) $\lnot A \to \lnot (A \lor \lnot A)$ --- axiom Ax.1 and 1) by mp

7) $\lnot \lnot A$ --- 5) and 6) and axiom Ax.10 by mp twice

8) $A$ --- from 7) by Double Negation Elimination : $\vdash \lnot \lnot \varphi \to \varphi$

Now we need Deduction Theorem (we can avoid it with more effort...) :

9) $\vdash \lnot (A \lor \lnot A) \to \lnot A$ --- from 1) and 4)

10) $\vdash \lnot (A \lor \lnot A) \to A$ --- from 1) and 8)

11) $\vdash \lnot \lnot (A \lor \lnot A)$ --- from 10) and 11) and Ax.10 nt mp twice

12) $\vdash A \lor \lnot A$ --- from 11) by DN-elim.