If a result is apparently provable with AC, is actually independent of ZF? Given the number of results that are independent of ZF. It seems that once you've found a proof of a theorem that uses the axiom of choice, the odds are that it will be independent of ZF. So my question is:
-Is there any result that has a solution in ZFC which relies on AC, but has another proof that can be done only in ZF?
I'm especially interested in those results which people thought that were going to be independent of ZF, because only a proof relying on AC was known. And then someone found a proof in ZF.
When I say axiom of choice I'm also including weaker versions like countable choice or DC.
 A: Construction of the Haar integral for locally compact Hausdorff group $G$ ... as a linear functional on $C_{00}(G)$ ... is often done using the Axiom of Choice.  In the Hewitt & Ross textbook ABSTRACT HARMONIC ANALYSIS this is Theorem (15.5), and they do it without AC.  They do then have an exercise (15.25) where they outline the much shorter proof using Tihonov's Theorem.
A: The paper "Division by Three" by Doyle and Conway (link to PDF) gives a proof of the following result without appeal to the axiom of choice:
Let $A$ and $B$ be sets, and let $3$ denote a three-element set.  If there exists a bijection from $3\times A$ to $3\times B$, then there exists a bijection from $A$ to $B$.
(This result is not due to Doyle and Conway -- it was first obtained by Lindenbaum and Tarski in 1926.)
A: Tarski proved that, for any set $A$, the set $W(A)$ of well-orderable subsets of $A$ has strictly larger cardinality than $A$.  This is trivial with AC, as then $W(A)$ is the whole power set of $A$ and thus Cantor's theorem applies.  But Tarski gave a proof that avoids AC.
I don't have my copy of Howard and Rubin's "Consequences of the Axiom of Choice" handy, but if I did then I could probably find lots of examples by looking at the various forms numbered 0A, 0B, etc.  I believe all of these are provable without AC (hence the number 0) but there was once a reason to suspect AC was needed.
A: There are many such proofs which use $AC$, but which are not even close to being independent of $ZF$. The general reason for this is how $AC$ is used. Normally the non-essential use of $AC$ appears when you have a very targeted application in mind, with additional structure in the background.
For example: Given an arbitrary collection of non-empty sets $\{X_\alpha: \alpha \in Y\}$ asserting that the product $Z =\Pi_{\alpha \in Y} X_{\alpha} $ is non-empty requires $AC$ when you have no structure imposed on the $X_\alpha$ and $Y$. However, when we add the assertion that each $X_\alpha$ is a ring, with additive identity $0_\alpha\in X_\alpha$, we then know that $Z$ is always non-empty without $AC$. The reason for this is because we now can define a function which witnesses that $Z$ is non-empty, in fact the function $\varphi:Y \rightarrow \bigcup X_\alpha$, given by $\varphi(\alpha) = 0_\alpha$ is such a witness, because $\varphi \in Z$.
That having been said, as for a specific example of a theorem for which everyone thought relied on $AC$ but was proven to hold in $ZF$, I cannot think of one off-hand that has not already been mentioned. But I think an example of what you are looking for might be contained in a question by Andres Caicedo, Distinct well-orderings of the same set and in his insightful answer to his own question.
