Is there a theorem whose only known proof uses "$A$ or not $A$" for undecidable $A$ Is there a known theorem $T$ in $ZF+DC$ (or $ZF$ or $ZFC$) such that the only proof we know of $T$ is by using the LEM applied to $A$ ( "$A$ or not $A$" ), where $A$ is independent of $ZF+DC$ ?  
 A: $T:= CH \vee \lnot CH$. 
Or, let $S$ be your favorite theorem, and consider $T:= S\wedge (CH\vee \lnot CH)$. 
A: Here is an example:

It is provable from $\sf ZF$ that there exists four infinite cardinals, $\frak p,q,r,s$ with $\frak p<q, r<s$ such that $\frak p^r=q^s$. (Here cardinals do not mean just finite ordinals and $\aleph$ numbers.)

You can find the proof here.
The proof using the axiom of choice is easy, and the proof not using the axiom of choice begins by using the fact that there is a set which cannot be well-ordered in order to construct the example.
Of course, the axiom of choice is indepedendent of $\sf ZF$. I also don't know an explicit proof of this theorem (in fact, before seeing this in a a math.SE question, I don't know if someone had proven this outside of a $\sf ZFC$ context either).
A: When I was in grad school I learned about the following fact which was actually intended as a joke.  
Theorem: There are irrational numbers $x$ and $y$ such that $x^y$ is rational.
Proof.  Look at $\sqrt2^{\sqrt2}$.  Is it rational?  If so, take $x=y=\sqrt2$, and we are done.  Otherwise, take $x=\sqrt2^{\sqrt2}$ and $y={\sqrt2}$, and we are again done since 
  $$x^y = \left(\sqrt2^{\sqrt2}\right)^{\sqrt2} = \sqrt2^{\left(\sqrt2\times\sqrt2\right)} = \sqrt2^2 = 2.$$
QED
I have no idea if the rationality of $\sqrt2^{\sqrt2}$ is decidable or not (most likely it is), so this is not quite an answer.
A: Another example is: Mycielski proved in 1964 under ZF that there is some $A \subseteq \omega_1^{\omega}$ such that the two-player game with payoff set in $A$ is not determined. The proof uses that either the axiom of determinacy fails, in which case this is easy, or else the axiom of determinacy holds, in which case there is no injection from $\omega_1$ into $\mathbb{R}$.
See exercise 27.12 in Kanamori "The Higher Infinite" for a short proof.
A: In this 1978 paper, Shelah and M. Rudin have proven that for each cardinal $\kappa$, there exists $2^{2^{\kappa}}$ many Rudin-Keisler incompatible ultrafilters on $\kappa$.
In the case that $2^{2^{\kappa}}>(2^{\kappa})^{+}$, the result follows from the free set lemma. The case where $2^{2^{\kappa}}=(2^{\kappa})^{+}$ has been proven separately by Shelah.
A: This 1991 paper in the Proceedings of the AMS presents the following result of Shelah: there exists a regular topological space of size $>\aleph_2$ in which there are no closed sets of size $\aleph_2$. 
If $2^{2^{\aleph_0}}>\aleph_2$, then $\beta\omega$ will serve; otherwise $\diamondsuit_{\{\alpha<\omega_2:cf(\alpha)=\aleph_0\}}$ holds, and this  can be used to construct a suitable topology on $\aleph_2^{\aleph_2}$. 
Math Reviews: MR1052572 
