http://en.wikipedia.org/wiki/Hahn-Banach_theorem#Relation_to_the_axiom_of_choice

> As mentioned earlier, the axiom of
> choice implies the Hahn–Banach
> theorem. The converse is not true. One
> way to see that is by noting that the
> ultrafilter lemma, which is strictly
> weaker than the axiom of choice, can
> be used to show the Hahn–Banach
> theorem, although the converse is not
> the case. The Hahn–Banach theorem can
> in fact be proved using even weaker
> hypotheses than the ultrafilter
> lemma.[4] For separable Banach spaces,
> Brown and Simpson proved that the
> Hahn–Banach theorem follows from WKL0,
> a weak subsystem of second-order
> arithmetic.[5]