Here's Theorem 4.3-2 (i.e. the Hahn Banach theorem for normed spaces):
Let $f$ be a bounded linear functional defined on a subspace $Z$ of a normed space $X$. Then there exists a bounbed linear functional $\tilde{f}$ on $X$ such that $$\tilde{f}(x) = f(x) \ \mbox{ for all } \ x\in Z,$$ and $$\Vert \tilde{f} \Vert_X = \Vert f \Vert_Z, $$ where $$\lVert f \rVert_Z := \sup \left\{ \frac{ \lvert f(x) \rvert }{\lVert x \rVert} \colon x \in Z, x \neq 0 \right\} \ \mbox{ if } Z \neq \{ 0 \}; \\ \mbox{ otherwise } \lVert f \rVert_Z := 0.$$ And, $$\Vert \tilde{f} \Vert_X \colon= \sup \left\{ \ \frac{ \vert \tilde{f}(x) \vert }{\Vert x \Vert} \ \colon \ x \in X, \ x \neq 0 \ \right\}.$$
I think I'm clear about the proof of this beautiful result. It uses the Hahn Banach Theorem for Complex Vector Spaces, which uses the Hahn Banach Theorem for Real Vector spaces, and the latter uses the Zorn's lemma.
Now if $X$ is a separable normed space, then is there a proof of the above result that doesn't involve the use of the Zorn's lemma?
Edit: This is all totally wrong. Well, the proof I had in mind uses AC although it might not be obvious that it does so, so it seems worth explaining that. But it's been pointed out that AC can be avoided. Thanks to Andreas Blass (some time ago I said he should post an answer to replace mine, he never did.) First the original, explaining where AC is used, then how to avoid it:
Original:
The separable case still requires some form of the Axiom of Choice, although it's less clear why.
Say $(x_n)$ is a dense sequence of elements of $X$. Say $Z_n$ is the span of $Z$ and $x_1,\dots,x_n$.
Now you simply extend your functional to $Z_1,$ then to $Z_2$, etc. You find you've extended it to the union of the $Z_n$, which is dense in $X$, and now since the extension is uniformly continuous on bounded sets you're done.
Where does AC come in? Well, first you "choose" an extension to $Z_1$, of the possibly infinite number of possible extensions. Then you "choose" an extension to $Z_2$... you have infinitely many choices to make.
EDIT: But you don't really need AC. Start by enumerating the rationals $r_1,\dots$. At each stage in the construction the proof gives you an interval $[a,b]$ such that if you define the value of the functional at $x_n$ to be anything in $[a,b]$ then the norm does not increase. If $a=b$ there is no choice to be made. If $a<b$ choose the $r_j\in[a,b]$ with $j$ minimal.