This is a bit late, but here is one example I like: <b>Theorem.</b> A localization of a regular local ring at a prime ideal is still regular. One way to prove this is to deduce it from <b>Theorem.</b> Let $R$ be a local ring. Then the following are equivalent: 1. $R$ is regular 2. Every $R$-module has a finite length projective resolution 3. The residue field has a finite length projective resolution. (To use it, let $P$ be the prime ideal. Since $R$ is regular, $R/P$ has a finite length projective resolution. Now localize--this is exact, so we get a finite length $R_P$-projective resolution of $(R/P)_P$, which is the residue field of $R_P$) This stuff is in Chapter 19 of Eisenbud's <i>Commutative Algebra</i>. It's not clear to me how one would try to prove the first theorem from the definitions of regular. Edit: fixed some mistakes