My favourite example is from Reverse Mathematics, namely Pincherle's theorem stating that

a locally bounded function on Cantor space is bounded there.

The obvious proof proceeds by contradiction and uses AC:

1. Suppose $F:2^\mathbb{N}\rightarrow \mathbb{N}$ is unbounded, i.e. $(\forall n\in \mathbb{N})(\exists f \in 2^{\mathbb{N}})(F(f)>n)$.

2. Apply (countable) choice to obtain a sequence $(f_n)_{n\in \mathbb{N}}$ such that $F(f_n)>n$ for all $n \in \mathbb{N}$.

3. Use the sequential compactness of Cantor space to show that this sequence has a subsequence $(g_n)_{n\in \mathbb{N}}$ which converges to $g\in 2^\mathbb{N}$.

4. Since $F$ is locally bounded, $F$ is bounded in a neighbourhood of $g$. However, as $n$ increases, $g_n$ approaches $g$ and $F(g_n)$ becomes arbitrary large. Contradiction.

There is a proof in ZF (and weaker systems) that is more delicate:

in step 2., one considers:

$(\forall n\in \mathbb{N})(\exists \sigma\in 2^{<\mathbb{N}})[(\exists f \in 2^{\mathbb{N}})(F(f)>n) \wedge \sigma = (f(0),..., f(|\sigma|) ]$.

One can apply `numerical choice' to obtain a sequence $(\sigma_n)_{n\in \mathbb{N}}$ such that:

$(\forall n\in \mathbb{N})[(\exists f \in 2^{\mathbb{N}})(F(f)>n) \wedge \sigma_n = (f(0),..., f(|\sigma_n|) ]$.

This `numerical' choice principle is provable in ZF. Now use the sequence $(\sigma_n)_{n\in \mathbb{N}}$ instead of the sequence $(f_n)_{n\in \mathbb{N}}$; the rest of the proof then can be modified to obtain a contradiction on the same way.