Compact Hausdorff Tychonoff is equivalent to BPI

A proper ultrafilter $V$ on a set $S$ decides every subset $A$: if $A\mathrm{\notin }V$, maximality says the filter generated by $V\cup \{A\}$ contains the empty set. Thus some $B\in V$ is disjoint from $A$, so $S\setminus A\in V$. Both cannot occur. If $S$ is compact, the closed sets $\bar{B}$, $B\in V$, have FIP: any finite intersection contains the nonempty intersection of the corresponding members of $V$. F5 gives a point $s$ in all these closures. Every open neighborhood $N$ of $s$ belongs to $V$, since otherwise the closed complement belongs to $V$, contradicting $s\in \overline{S\setminus N}=S\setminus N$. When $S$ is Hausdorff there is at most one such limit: two distinct limits have disjoint neighborhoods, which cannot both be in a proper filter. Hence each ultrafilter on a compact Hausdorff space has a unique limit.

Assume BPI and that each $X_i$ is nonempty. Let $E$ be the set of all functions $s$ with finite domain contained in $I$ and $s(i)\in X_i$ on their domains. The empty function belongs to $E$. For a finite $J\subseteq I$ put $D_J=\{s\in E:J\subseteq \mathrm{dom}s\}$. This set is nonempty by finite choice in ZF; explicitly, induction on the size of $J$ extends a partial selection by one element from the next nonempty factor. Moreover $D_J\cap D_K=D_{J\cup K}$ and $D_{\mathrm{\varnothing }}=E$. Their supersets form a proper filter, which F1 extends to an ultrafilter $W$ on $E$.

Separately, assume compactness of all products of compact Hausdorff spaces. Given a finitely satisfiable set $\mathrm{\Gamma }$ of propositional formulas with letters in a set $P$, take $2^P$ with discrete two-point factors. Each factor is compact (an open cover has a subcover with at most two members) and Hausdorff (the two singletons separate its points), so the assumed principle makes $2^P$ compact. The space is nonempty even without the principle, since the constant-zero function is a valuation. For a finite formula $\varphi$, its truth set $C_{\varphi }$ is clopen: a letter's truth set is a coordinate singleton cylinder, negation takes complements, and conjunction and disjunction take finite intersections and unions. This structural induction applies also to truth constants, whose sets are the whole cube and the empty set. Finite satisfiability says precisely that the $C_{\varphi }$, $\varphi \in \mathrm{\Gamma }$, have FIP. F5 gives a point satisfying all of $\mathrm{\Gamma }$. By F2, BPI follows.

Returning to the BPI assumption in step 1.2, for $i\in I$ and $A\subseteq X_i$, put $A^{(i)}=\{s\in D_{\{i\}}:s(i)\in A\}$ and $V_i=\{A\subseteq X_i:A^{(i)}\in W\}$. These sets form a proper filter: inverse images preserve intersections and inclusions, $X_i^{(i)}=D_{\{i\}}\in W$, and ${\mathrm{\varnothing }}^{(i)}=\mathrm{\varnothing }\mathrm{\notin }W$. The two sets $A^{(i)}$ and $(X_i\setminus A{)}^{(i)}$ partition the $W$-large domain $D_{\{i\}}$. By step 1.1 exactly one is in $W$, so $V_i$ is an ultrafilter: adjoining any missing $A$ contradicts its already present complement. Step 1.1 supplies its unique limit $x_i\in X_i$. Replacement on this unique specification gives the function $i\mapsto x_i$ in ZF. It is an element of $X={\prod }_i{X}_i$, proving nonemptiness without choosing from a family of multiple limit points.

To prove compactness of this nonempty product, let $\mathcal{C}$ be a closed FIP family in $X$. The sets containing a finite intersection from $\mathcal{C}$ form a proper filter; F1 extends it to an ultrafilter $U$. For each $i$, the family $\{A\subseteq X_i:{\pi }_i^{-1}[A]\in U\}$ is an ultrafilter by inverse-image identities and the decision property in step 1.1. Its unique limit $y_i$ again defines a product point $y$. Each basic neighborhood of $y$ is a finite intersection of inverse images of coordinate neighborhoods, all of which belong to $U$. Thus every neighborhood of $y$ is in $U$. For $C\in \mathcal{C}$, if $y\mathrm{\notin }C$, its open complement would be in $U$ together with $C$, a contradiction. Therefore $y\in \bigcap \mathcal{C}$, and F5 proves compactness.

If a factor is empty the product is empty by F4 and is compact, since the empty subfamily covers it. If $I=\mathrm{\varnothing }$, F4 makes the product a singleton, which is nonempty and compact: any cover has a member containing its one point. These observations cover the cases omitted when constructing partial selections and coordinate limits. The empty family of constraints in step 1.3 is satisfied by the constant-zero valuation, including the empty valuation when $P=\mathrm{\varnothing }$. QED.