Under dependent choice a normal $T_1$ space is completely regular, so $T_4 \Rightarrow T_{3\frac{1}{2}}$, and together with the implications already proved this is the whole classical chain

Assume the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain). If $(X,\mathcal{T})$ is normal and $T_1$, that is $T_4$ (Normal spaces and $T_4$ spaces, with the source disagreement over whether normality includes $T_1$ stated explicitly, $T_0$ (Kolmogorov) and $T_1$ (Frechet) spaces), then $X$ is completely regular (Completely regular spaces and Tychonoff ($T_{3\frac{1}{2}}$) spaces). Since $X$ is also $T_1$, $X$ is Tychonoff, and $T_4 \Rightarrow T_{3\frac12}$.

Combined with The implications proved on this page: perfectly normal gives completely normal under countable choice, and completely normal gives normal; normal with $T_1$ gives $T_3$; completely regular gives regular; regular with $T_1$ gives Urysohn, hence Hausdorff, hence $T_1$, hence $T_0$; and metrizable gives every one of them, every arrow of

$T_6 \Rightarrow T_5 \Rightarrow T_4 \Rightarrow T_{3\frac12} \Rightarrow T_3 \Rightarrow T_{2\frac12} \Rightarrow T_2 \Rightarrow T_1 \Rightarrow T_0$

now holds: the first arrow under the Axiom of Countable Choice (The Axiom of Countable Choice ($\mathrm{AC}_\omega$)), the arrow $T_4 \Rightarrow T_{3\frac12}$ proved here under dependent choice, and every other arrow with no choice principle at all. No arrow of this chain is asserted to reverse.

• This corollary supplies exactly the one arrow the published separation-axioms page could not reach. That page's own rem-separation-axiom-conventions names the missing arrow as normal $T_1$ implies completely regular and records that no rearrangement of material already on that page could supply it, since the implication is Urysohn's lemma. Nothing in this corollary revisits or amends that page; it only supplies, at a later point in the reading order, the theorem that page named as absent.

• The chain above is not asserted to be a theorem of ZF. Its weakest link is this corollary's own dependent-choice hypothesis, and the first arrow separately costs countable choice; neither cost is removed by combining the arrows, and no clause of The implications proved on this page: perfectly normal gives completely normal under countable choice, and completely normal gives normal; normal with $T_1$ gives $T_3$; completely regular gives regular; regular with $T_1$ gives Urysohn, hence Hausdorff, hence $T_1$, hence $T_0$; and metrizable gives every one of them is reproved here.