The Hahn-Banach Theorem (HB) cannot be proved without some version of the Axiom of Choice. (Technically, it's stronger than ZF but weaker than BPI.) A cool fact about HB is that it is sufficient for proving the existence of nonmeasurable sets and even for proving the Banach-Tarski paradox.
In 1969, Luxemburg proved that the Hahn-Banach theorem is equivalent to the claim that every boolean algebra has a (finitely additive) probability measure.
He also proved that the Hahn-Banach theorem is also equivalent to the following interesting claim:
- For any set Ω and proper ideal N of subsets of Ω (i.e., N is closed under finite unions, any subset of a member of N is a member of N, but not every subset of Ω is in N), there is a (finitely additive) probability measure on all subsets of Ω that is zero on every member of N.
- Any boolean algebra is isomorphic to the quotient of a boolean algebra of sets.
(This is part of a general observation that some of the things that can be done with ultrafilters can also be done with filters, though the results may be weaker.)