# Proof with axiom of choice implies proof without?

Is there a theorem that guarantees the existence of a proof not using AC given there is a proof using AC, at least under some circumstances? What is its name (if there is one) and its most general form?

This of course excludes the trivial cases for example a finite collection of non-empty sets.

-
An enormous number of consequences of AC are specifically known to be independent of ZF, so I rather think that such a result will be either very technical or too narrow to be of much interest. –  Brian M. Scott Mar 9 '12 at 15:07

Among other things, it shows that any $\Pi_2^1$ sentence of Peano Arithmetic that (with the usual translation) can be proved in ZFC can already be proved in ZF. (That had already been shown much earlier by Gödel. Shoenfield's result is stronger.) The $\Pi_2^1$ sentences include well-known open problems such as the Goldbach Conjecture, the Riemann Hypothesis, $\text{P}=\text{NP}$, many more.
It is not worth editing the answer, but just to clarify potential future confusion, usually $\Pi^1_2$ sentences are considered in second-order arithmetic, and Peano arithmetic is formalized so that it only has arithmetical ($\Sigma^0_\infty$) sentences. –  Carl Mummert Mar 11 '12 at 12:13