Many examples from set theory are known, but here is a very basic (third-order) theorem from most ordinary mathematics:

"A regulated$f:[0,1]\rightarrow \mathbb{R}$ is bounded", (&)

where 'regulated' means that the left and right limits $f(x-)$ and $f(x+) $ exist everywhere.

To prove (&) using (countable) Axiom of Choice and (basic) sequential compactness, suppose there is a regulated $f:[0,1]\rightarrow \mathbb{R}$ that is not bounded. Find a sequence $(x_n)_{n\in \mathbb{N}}$ in $[0,1]$ such that $f(x_n)>n$ for all natural numbers $n$. This sequence has a convergent sub-sequence, say with limit $y\in [0,1]$. Then either $f(y-)$ or $f(y+)$ does not exist, and we are done. This proof only uses countable choice for quantifier-free formulas (called QF-AC$^{0,1}$ by Kohlenbach) and arithmetical comprehension.

One can also prove (&) without using the Axiom of Choice, namely in Z$_2^\Omega\equiv$ RCA$_0^\omega+(\exists^3)$; here, RCA$_0^\omega$ is Kohlenbach's base theory from higher-order reverse mathematics and $(\exists^3)$ is Kleene's quantifier. The system Z$_2^\Omega$ is a conservative extension of Z$_2$ and a fragement of ZF. Intuitively, one cannot prove (&) in fragments of Z$_2^\Omega$. The proof of (&) in Z$_2^\Omega$ is fairly indirect and involved, via a supremum principle and the Heine-Borel theorem for uncountable coverings.

In conclusion, the Axiom of Choice makes (&) much easier to prove in a much weaker system.

Finally, the aforementioned negative results (and many more examples) can be found in:

https://arxiv.org/abs/1808.09783

https://arxiv.org/abs/1910.02489

https://arxiv.org/abs/2212.00489

A Platonist will appreciate the observation that a well-known phenomenon (AC simplifies proofs, even when not needed) from the foundations of mathematics is reflected in ordinary mathematics. Comparisons with Plato's cave are allowed.