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.