It can be proven without any form of infinite choice that the product of two compact spaces (and thus any finite product) is compact, while on the other hand, it is well known that the general form of Tychonoffs theorem implies the axiom of choice.
So a general formulation of this question would be: Is there a proof of Tychonoffs theorem where the use of AC/Zorn's lemma can be reduced to using the axiom of dependent choice up to the ordinal that indexes the product? With the case of countable products being of particular importance.