Is there a proof of LEM implying DNE that doesn't use $\bot\vdash\varphi$? Is there a proof not using $\bot\vdash\varphi$, proving that Law of The Excluded Middle implies Double Negation Elimination in natural deduction? The ones I've seen would use $\bot\vdash\varphi$ at some point.
 A: Couple of thoughts:
First, any question like 'is there a proof ...' should always be couched relative to some proof system. i.e you should really ask 'Is there a proof system in which there exists a proof ...'
Second, when you ask for a proof that LEM implies DNE ... that's a little weird, since in classical logics DNE holds without making any further assumptions. That is, for all complete systems $S$ for classic propositional logic we have $\vdash_S \neg \neg \phi \rightarrow \phi$
EDIT: From the comments I understand you are looking for a proof that does not use LEM (nor $\bot \rightarrow \phi$ ... I'll refer to that rule as $\bot$ Elim) as one of its steps.  OK, below is a proof done in Fitch, where $\neg$ Elim is defined as going from $\neg \neg \phi$ to $\phi$, so that doesn't use LEM or $\bot$ Elim:

Finaly, if you're looking for a system where you do have to derive $\neg \neg \phi \rightarrow \phi$, but that still does not use LEM or $\bot$ Elim, I point you the Hilbert system, which does not have LEM or $\bot$ Elim as its rules, but you can prove $\neg \neg \phi \rightarrow \phi$ in that system nevertheless.
A: If we look at this from the perspective of something like intuitionistic natural deduction, I don't believe so.
First, recall that we can take negation to be non-primitive, i.e. ($\neg P := P \rightarrow \bot$).  Recall also that $\bot$ has no intro rules and a single elimination rule which corresponds to $\bot \vdash \varphi$.  Thus, if we remove this rule, we're basically treating $\bot$ like an arbitrary formula.  It seems to me then that a proof of LEM implying DNE should hold if we sub out $\bot$ for some arbitrary $Q$.  Doing this to LEM yields to scheme $P \vee (P \rightarrow Q)$, and DNE yields $((P \rightarrow Q) \rightarrow Q) \rightarrow P$.  Notice that the first is a classical tautology and the second is not even valid classically.  Since we then can't prove this implication classically, we certainly won't be able to do it intuitionistically.
