Is there a theorem whose only known proof uses "$A$ or not $A$" for undecidable $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).

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.

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.