What are some results in mathematics that have snappy proofs using model theory?

Plane geometry is decidable. That is, we have a computable algorithm that will tell us the truth or falsity of any geometrical statement in the cartesian plane.

This is a consequence of Tarski's theorem showing that the theory of real closed fields admits elimination of quantifiers. The elimination algorithm is effective and so the theory is decidable. Thus, we have a computable procedure to determine the truth of any first order statement in the structure (R,+,.,0,1,<). The point is that all the classical concepts of plane geometry, in any finite dimension, are expressible in this language.

Personally, I find the fact that plane geometry has been proven decidable to be a profound human achievement. After all, for millennia mathematicians have struggled with geometry, and we now have developed a computable algorithm that will in principle answer any question.

I admit that I have been guilty, however, of grandiose over-statement of the situation---when I taught my first logic course at UC Berkeley, after I explained the theorem some of my students proceeded to their next class, a geometry class with Charles Pugh, and a little while later he came knocking on my door, asking what I meant by telling the students "geometry is finished!". So I was embarrassed.

Of course, the algorithm is not feasible--its double exponential time. Nevertheless, the fact that there is an algorithm at all seems amazing to me. To be sure, I am even more surprised that geometers so often seem unaware of the fact that they are studying a decidable theory.

Hilbert's Nullstellensatz is a consequence of the model completeness of algebraically closed fields.

Edit: I don't have a reference, but I can sketch the proof. Suppose you have some polynomial equations that don't have a solution over ${\mathbb C}$. Extend ${\mathbb C}$ by a formal solution, and then algebraically close to get a field $K$. The field $K$ obviously contains a solution, but by model completeness of algebraically closed fields, a first-order statement is true in an algebraically closed field only if it is true in every algebraically closed field. The existence of a solution to a finite set of polynomial equations is a first-order statement and ${\mathbb C}$ is algebraically closed. QED.

Not sure if this is what you are looking for but Tychonoff's theorem has a snappy two line proof in the non-standard setting once the non-standard characterization of compact is established. The non-standard characterization of compactness says that $X$ is compact if and only if every $x\in X^\*$ is infinitely close to some standard point in $X$ and infinitely close is defined in terms of the monads of the topology.

Edit: (Tychonoff) $X := \prod_{i\in I}X_i$ is compact if and only if each $X_i$ is compact.

The forward direction is easy and does not require any non-standard analysis. Simply use the projection maps.

Now suppose all the $X_i$ are compact and let $y\in X^\*$ then $y(i^*)\in (X_i)^*$. Since $X_i$ is compact there is some $x(i)\in st(y(i^\*))$ and we can take $x\in X$ to be the product of the points $x(i)$. By construction $x^*\approx y$ and this establishes the backward direction.

The above theorem along with its non-standard proof can be found in "Nonstandard Analysis" by Martin V$\ddot{a}$th on page 166 but I'm sure any other book on the subject will include a proof of the theorem using pretty much the same terminology and concepts.

Notation: $(-)^\*$ is the extension map, $st(-)$ is the standard part map, and $\approx$ is the relation defined in terms of the monads of the topology.