What is the Implicit Function Theorem good for?

One of the major applications of Implicit Function Theorem is the lesson it teaches:

                      Locally, Manifold Theory = Linear Algebra. 

That is, locally, we can perform our calculus as if it is linear algebra. Solving simultaneous equations, discussing about linear independence of coordinates, basis set and mapping from one manifold to another can be viewed as linear transformations. Discuss the invertibility of functions as if they are linear transformations. In fact by Darboux's theorem, in Symplectic manifold theory the linear algebra aspects are more prominent.

The infinite-dimensional implicit function theorem is used, among other things, to demonstrate the existence of solutions of nonlinear partial differential equations and parameterize the space of solutions. For equations of standard type (elliptic, parabolic, hyperbolic), the standard version on Banach spaces usually suffices, but you have to be clever about which Banach space to use. There is a generalization of the implicit function theorem, due to Nash who used it to demonstrate the existence of isometric embeddings of Riemannian manifolds in Euclidean space, that works for even more general types of PDE's. Moser stated and proved a simpler version of the theorem. There is a beautiful survey article by Richard Hamilton (who originally used the Nash-Moser implicit function theorem to prove the local-in-time existence of solutions to the Ricci flow) on the Nash-Moser implicit function theorem.

If you go a little bit further than the inverse and implicit function theorems, you can get a fairly practical theorem. Kantorovich's theorem gives you fairly strong sufficient conditions for a system of smooth equations to have a solution. Moreover it tells you how quickly Newton's method converges in that situation. For example, this theorem is used by Harriet Moser to prove that SnapPea does give approximations to actual solutions to the hyperbolic gluing equations. The applications of course are pretty broad, this is one on the fairly pure end of the spectrum. Kantorovich was an economist although I do not understand the economics problems he was interested in.

If you're interested, this perspective on the inverse and implicit function theorems is in "full glory" in Hubbard's multi-variable calculus text.

2nd answer: The proof of Sard's theorem is a delicate dance with the Implicit Function Theorem, Taylor's Theorem and some basic argument with Lebesgue measure zero.