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.