Hahn-Banach without Choice

The ultrafilter theorem is the statement that any filter on a set can be extended to an ultrafilter. It is perhaps more common to see it sated as the (Boolean) Prime ideal theorem: Every Boolean algebra admits a prime ideal.

The Hahn-Banach theorem is actually equivalent to the statement that every Boolean algebra admits a real-valued measure, but this is not entirely straightforward (see Luxemburg, "Reduced powers of the real number system and equivalents of the Hahn-Banach extension theorem", Intern. Symp. on the applications of model theory, (1969) 123-127).

For a discussion of Hahn-Banach vs. Choice and some additional remarks and references, see Jech "The axiom of choice", North-Holland, 1973.

You may also be interested in the references I include in this answer.

An amusing related fact is that the non linear Hahn-Banach theorem (that every Lipschitz one function into the reals from a subset of a metric space can be extended to a Lipschitz one function on the entire space) is provable in ZF. I believe it is proved this way in the book of Araujo and Gine.

This might be irrelevant, but I would like to point out that if one restates Hahn-Banach theorem in the language of locales (replacing topological spaces), one can get rid of the axiom of choice and the ultrafilter theorem altogether. See the paper “A Direct Proof of the Localic Hahn-Banach Theorem” by Thierry Coquand and references therein.