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.