Every time I hear it mentioned it is praised in the highest possible terms, and I remember one of my old lecturers saying that it is one of the 3 most important theorems in analysis. Yet the only consequences of it that I have read is that it proves that there are lots of functionals and that separating hyperplanes exist. Are those 2 consequences really that spectacular, or are there other ones that I don't know of?

40$\begingroup$ I strongly recommend to reopen the question. $\endgroup$– GuntramMay 31, 2010 at 17:49

27$\begingroup$ if this is not a real question, I'm a ghost $\endgroup$– Pietro MajerMay 31, 2010 at 18:36

22$\begingroup$ How can this be considered not a real (pun intended) question? Not everyone reading this site has necessarily learned functional analysis. If someone asked here why the fundamental theorem of calculus is important, that's below the level of the site, but a major theorem in advanced mathematics? Please reopen. $\endgroup$– KConradMay 31, 2010 at 20:30

14$\begingroup$ This is a real question, if for no other reason because it has good answers. Please reopen it. $\endgroup$– Andrej BauerMay 31, 2010 at 21:05

30$\begingroup$ Meta thread: tea.mathoverflow.net/discussion/418/… $\endgroup$– Andrew StaceyJun 1, 2010 at 7:06
7 Answers
I have used it (sometimes with coauthors) several times in the following general context. I have wanted to prove that a function f can be decomposed as a sum g+h, where g has certain properties and h has certain properties. It has been possible to show that the set of acceptable g is convex, as is the set of acceptable h. So I'm trying to show that f belongs to a sum of two convex sets K+L. But a sum of convex sets is convex, so if f cannot be written in such a way, then it can be separated from K+L by a functional. It is often possible to derive a contradiction from this.
The result is that one can prove the existence of the desired decomposition under circumstances where explicitly defining a decomposition would be difficult.
Incidentally, the applications I am alluding to are of the finitedimensional HahnBanach theorem. Some people call it the minimax theorem, and still others would call it duality for linear programming or something like that.
My two cents.
Linear functionals on a Banach space B are used to define the dual space B', and the weak topology on both the space and on its dual. But of course you need sufficiently many functionals to get an interesting object and topology. The theorem of HahnBanach implies that the weak topology is Hausdorff, and it definitely seems to be a prerequisite to get something useful. Now the weak topology on B is often more suitable than the norm topology on B in practical applications because it has "more" compact sets . Think of a Hilbert space, or a reflexive Banach space. Its unit ball is compact with respect to the weak topology. This gives rise to many existence theorems in several fields of mathematics. Think also of the space of distribution $D'(R)$. Here again the weak topology seems to be more useful than its intrinsic topology.
Let me give another reason. Linear functionals can be seen as an infinite dimensional equivalent of the coordinates in $R^n$. I think that you will agree that the introduction of coordinates systems to represent points in space was a big leap forward in mathematics, from the historical viewpoint. Here is a problem that illustrates the need for coordinates in functional analysis. Let B a Banach space. You want to give a meaning to the integral of a Bvalued function. Certainly, you want linearity, that is $\lambda(\int f d\mu)= \int(\lambda(f)d\mu)$, for all linear functional $\lambda$ on B. That's integration "coordinates by coordinates". It is not always possible to define such an integral, but the HahnBanach theorem tells you that there is only one possible value for $\int f d\mu$ if linearity holds.

3$\begingroup$ Dude(tte), you've just made Bvalued integration make a lot more sense to me. Thanks! $\endgroup$– PietroMay 31, 2010 at 23:43

$\begingroup$ Thanks for clarity and humility ! For those who have closed this question...It's not a good choice. $\endgroup$ May 4, 2014 at 12:34
Here are a few more consequences:
 The norm of $T^*$ equals the norm of $T$
 $X$ reflexive and $M$ closed in $X$ implies $M$ reflexive
 If $X$ Banach then $X^*$ reflexive iff $X$ is reflexive
 $X^*$ separable implies $X$ separable
 If $X$ Banach and $T \in B(X)$ then $T$ invertible iff $T^*$ invertible
HahnBanach is fundamental as a mean to easily obtain existence of objects in functional analysis. Basically, it expresses that any problem of a certain type which has no "obvious obstructions" has a solution. Even in finite dimensions, it is at the heart of the powerful duality in convex optimization (or the properties of the LegendreFenchel transformation).
HahnBanach is also equivalent to the lower semicontinuity in the weak topology of convex semicontinuous functions, which allows to obtain solutions of many variational problems via minimization, for instance when sublevels of the convex functional are weakly compact. On the other hand, you have to work harder (use other input, e.g. regularity theorems) to state anything above the mere existence of your solution.
Interestingly, from this angle, Jean Dieudonné in his huge treatise on analysis gets away without it (IIRC). He makes part of it into an exercise? The reason being, apparently, that he approaches analysis from the "separable metric space" attitude, which he justifies somewhere. It's an interesting thing, therefore: it is one of the four canonical ideas in functional analysis (as said by F. Riesz?), but if you don't accept that mindset, there may be other ways. You are still going to need some existence principle for linear functionals.
Let me give you a "real life" example of a use of the HahnBanach theorem. In one of my papers I needed the classification of the maximal subsemigroups of $\mathbb{Z}^n$. In the paper where the classification was done there was an unproved statement that didn't seem trivial to me. To prove it I needed a version of the HahnBanach theorem. So even an algebraist like me had to use it. If a theorem is useful outside its original area, it is probably quite important.