Amount to choice necessary to prove instances of Tychonoff theorem

Question

Let $I$ be a fixed nonempty set. I would like to know how much choice is necessary in order to prove that the product of any $I$-indexed family of compact topological spaces is compact (under the product topology). The usual proof of Alexander subbase theorem gives no information about that, because it is based on Zorn's lemma.