Reference: http://web.mat.bham.ac.uk/C.Good/research/pdfs/horror.pdf
It is well known that the original proof of Urysohn's lemma uses a choice principle. (DC)
What are weak forms of the Urysohn's lemma that don't require choice? For example, one is in the link. ($\text{ Second Countable } + \text{ Regular } \Rightarrow \text{ Urysohn's lemma }$)
I also saw somewhere (I don't remember) that Urysohn's Lemma is provable without choice if it is metric space. (Edit; Now I remember. It was an exercise on PMA, using Hausdorff distance)