Double negation vs. law of excluded middle? I think I am operating under classic logic here, or propositional logic? Not sure if these are the same thing or what all the options are here.

When I see how to prove double negation elimination, it uses law of excluded middle. When I see how to prove law of excluded middle, it uses double negation elimination.

Are these two things considered equivalent and axiomatic or is there some other proof that handles both? If it is an axiom, what other axioms exist?
In a propositional logic, the sentences are built out of primative abstract sentences $A_1,A_2,\ldots $ by combining them with connectives. The usual set of connectives are $\{\lnot,\land,\lor,\to, \leftrightarrow\},$ though sometimes a smaller set is used (or a smaller set is taken as primative and the others are defined off of them). Sometimes also there are other connectives too (e.g. in modal propositional logic), but since we're only really focusing on classical and intuitionistic here, which only use the ones I mentioned.

So things like $A_1\to A_2$ and $A_1\lor \lnot A_3$ would be sentences. Here we would write the law of excluded middle as $$ \mathcal A \lor \lnot\mathcal A$$ where it's understood that we can substitute any given sentence for $\mathcal A.$ Such a substitution is called an instance of LEM, so, for instance $ (A_1\land A_2)\lor \lnot(A_1\land A_2)$ is an instance of LEM.

The thing that makes the system "propositional" as opposed to, say, a predicate logic is that the basic building blocks are these primative abstract sentences $A_i.$ In predicate logic, the atomic sentences themselves have structure, and we have variables and constants representing individuals, and relation symbols representing relations between individuals (like equality), and quantifiers. For instance, you've probably seen things like $$\forall x_1 \forall x_2((x_1&lt;x_2)\land (x_2&lt;x_1)).$$ This is a sentence in predicate logic (that is also false in its usual interpretation as a sentence about numbers). 

Predicate logic is related to propositional logic cause we can still write things like LEM $$ \mathcal A \lor \lnot\mathcal A,$$ where now we will substitute sentences of predicate calculus in for $\mathcal A$ to generate instances. So we can talk about the LEM in either context. From now on, I'll stick to propositional logic.

Now, we've talked about the grammar, but we still haven't said what these sentences are for. Of course we know that we intend $A_1\to A_2 $ to mean what "if $A_1$, then $A_2$" informally means and $A_1\land A_2$ to mean "$A_1$ and $A_2$", etc. We want is to be able to prove certain sentences valid, for instance, clearly we would like to be able to show somehow $A_1\to A_1$... this is clearly something that "should" be valid.

So we need a deductive system, which consists of rules for taking valid sentences and producing new valid sentences, as well as axioms, sentences we assume are valid. There are tons of different ways to do this: the main systems fall into three categories: Hilbert-style systems, natural deduction, and sequent calculus. No time to explain what these are, of course, other than to say a natural deduction system will be most convenient for our purposes here, so that's the category you're seeing here, though it will usually be presented much more formally (and carefully).

In this, we will take as a primative axiom scheme that $\mathcal A\to \mathcal A$ is valid where anything is substituted for $\mathcal A.$ This will be the only axiom, and everything else will be rules. (EDIT: I actually don't think this axiom scheme is even necessary since every instance of it follows from the $\to$ introduction rule described below.)

For instance, we have an introduction rule for $\lor$ that if a sentence $\phi$ is valid then $\phi\lor \psi$ and $\psi \lor \phi$ are valid for any sentence $\psi.$ Then we have an elimination rule, that if from the assumption of validity of a sentence $\phi$, we can derive that $\psi$ is valid, and separately, if from the assumption of the validity of a sentence $\phi',$ we can derive that same $\psi$ is valid, and $\phi\lor \phi'$ is valid, then $\psi$ is valid.

We can define similar introduction and elimination rules for $\land$... I won't mention what they are for lack of space: they're easier than the ones for $\lor$ and you can probably figure out what they are. Then there is an introduction rule for $\to$: if starting with a hypothetical assumption of $\phi,$ we can derive that $\psi$ is valid, then $\phi\to \psi $ is valid. And then the elimination rule is that if both $\phi$ and $\phi\to \psi$ are valid, then $\psi$ is valid.

Finally, we come to negation. First off, it is most convenient to not take negation as primative, but rather to take special primative sentence $\bot$ which intuitively represents a false statement or a contradiction. Then we define negation as $\lnot \mathcal \phi = \mathcal \phi\to \bot.$ Then we have an elimination rule for $\bot$ that from $\bot$ we can infer any sentence, which formalizes the notion that from an absurdity, we can derive anything. There is no introduction rule for $\bot.$

Notice this gels with our intuitive idea of contradiction, because if we have $\phi$ and $\lnot \phi,$ which recall is just an abbreviation for $\phi\to \bot,$ then by $\to$ elimination, we infer that $\bot$ is valid.

These rules give a version of the deductive system for intuitionistic propositional logic. Any statement whose validity can be proven by these rules is called intuitionistically valid. As I mentioned before, there are many different types of deductive systems that all produce the same valid sentences... I have only given one example.

Now, here's where we finally get down to answering your question. We can convince ourselves that we can neither prove $A_1 \lor \lnot A_1$ nor $\lnot\lnot A_1 \to A_1$ from the above rules. (It's a bit more complicated than this if we want to be careful, but the basic idea for LEM is that in order to get $A_1\lor\lnot A_1,$ we'd need to use the introduction rule for $\lor,$ which requires that we have either $A_1$ or $\lnot A_1$ valid. And it's clear, since $A_1$ is just some abstract sentence, there's no way of proving either of these things.) 

So the schemes $\mathcal A \lor \lnot \mathcal A$ and $\lnot\lnot \mathcal A \to \mathcal A$ are not generally valid under intuitionistic logic. However, we can show that by taking either one of these schemes as an axiom, we can derive every instance of the other. So LEM and double negation elimination are equivalent over intuitionistic propositional logic. Adding either of these as an axiom results in classical propositional logic.
Two basic equivalences in classical logic are:

Double Negation

$$P \Leftrightarrow \neg \neg P$$

Implication

$$P \rightarrow Q \Leftrightarrow \neg P \lor Q$$

Thus, we have:

$$\neg P \lor P \Leftrightarrow P \rightarrow P \Leftrightarrow \neg \neg P \rightarrow P$$

Does that help?