A good number of theorems in Ramsey theory and related areas are what logicians call $\Pi^1_2$ statements—those of the form "for every set of integers $X$ there is a set of integers $Y$ satisfying some property which only quantifies over integers". Often, the easiest proofs of these results use AC, e.g. in the guise of using a nonprincipal ultrafilter or using nonstandard methods. But a consequence of Shoenfield's absoluteness theorem is that no theorem of this form requires choice for its proof.
A good example of this is Hindman's theorem (any finite coloring of $\mathbb N$ admits an infinite set whose set of finite sums is monochromatic). There's a very nice, quick proof through idempotent ultrafilters, which of course need (a fragment of) AC. There is an elementary proof, but it is much more involved and intricate, requiring you to do all the bookkeeping details by hand.
