When you invoke the axiom of choice, it is because whatever you need to choose consists of small parts you technically have to choose one by one. So if I need to use the axiom of choice, but subsequently prove that no matter what I choose the end result is the same, is there really a need for the axiom of choice?
This is where I bumped into the question: You have a set of abelian groups $G_i$ each with a given subgroup $H_i$, with $i\in I$ for some index set $I$. Show that the following isomorphism holds: $ \prod_{i\in I}\left(G_i/H_i\right) \approx\left(\prod_{i\in I}G_i\right)/\left(\prod_{i\in I}H_i\right). $ And here's my proof:
An element in $g\in \prod_{i\in I}\left(G_i/H_i\right)$ is given by a (possibly infinite) tuple of elements of each quotient group. Each coordinate in the tuple is represented by an element $g_i$ in the corresponding $G_i$, which means that we can use the representatives to make an element in $\prod_{i\in I}G_i$ (this requires the axiom of choice if $I$ is big enough).
Now, the difference between any two such elements is a tuple in $\prod_{i\in I}H_i$, so in the end what choice we make doesn't matter, any choice will give the same element in the final quotient group. But I still used the axiom to show that a representative existed, so my intuition says that this needs the axiom of choice, although I'm not certain.
I use the word "tuple" here, because that's how I think of direct products. Representing the product as a function from the index set into the disjoint union (which is the proper way) will give a completely analogous reasoning.