Examples of theorems that haven't been proven without AC in practice but can be proven without it in principle It is possible to prove theorems of the form "if $\phi$ is provable in ZFC, then $\phi$ is provable in ZF". For example, let $\phi$ be a statement that is absolute between $V$ and $L$. If $\phi$ were not provable in ZF, then there would be a model $M$ in which it is false, which in turn implies that it is false in $L^M$, hence not provable in ZFC.
I was wondering whether there are natural such statements all known proofs of which involve axiom of choice (or whose proofs become substantially easier when AC is used).
Following Andres Caicedo's answer and comments here, it is possible to "cheat" and turn ZFC proofs into ZF proofs by carrying out the argument in L and then using absoluteness. What I had in mind was to see if there are examples where AC "takes care" of a procedure which in theory we could do without it.

Here is some general theorem that you can prove.$\newcommand{\Ord}{\mathsf{Ord}}$
We write $(\exists^{\Ord}x)\varphi$ and $(\forall^{\Ord}x)\varphi$ to mean that we are bounding the quantifier on $x$ as a set of tuples of ordinals. Meaning $x\subseteq\Ord^{<\omega}$, and $\varphi$ holds. (You can observe that this doesn't increase the complexity of the formula in the Levy hierarchy more than a usual quantifier would.)
If $\varphi(x)$ is a statement which is upwards absolute, then $(\forall^\Ord x)\varphi(x)$ is provable with the axiom of choice if and only if it is provable without the axiom of choice. The proof is almost trivial, given $x\subseteq \Ord^{<\omega}$, we can consider $L[x]$ as a model of choice, $\varphi(x)$ holds there, and it is upwards absolute, so it holds in $V$. $\qquad\square$
This gives an immediate plethora of examples in the sense of finite coloring theorems and properties, e.g. "every coloring of a subset of $[\kappa]^{<\omega}$ in $\lambda$ colors, has a subset of order type/cardinality $\alpha$ which is homogeneous/anti-homogeneous" are all statements of the form $\Pi_2$ whose universal quantifiers can be replaced by $\forall^\Ord$.

You can also take a look in Herrlich's book The Axiom of Choice which includes many examples of less set-theoretical nature.
