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.

globalcontinuity are equivalent for real functions. See the answers on Mathematics: Continuity and the Axiom of Choice. This result is in the chapter named "Unnecessary Choice" in Herrlich's book - maybe some other results from that chapter might be interesting, too. It is mentioned in one of the answer here: Unnecessary uses of the axiom of choice. $\endgroup$