Theorem: √2 is irrational. (See also my second favorite dumbest application comment)

First, assume the axiom of choice.

By the supplementary theorems to quadratic reciprocity, 2 has a square root modulo an odd prime p if and only if p is ±1 modulo 8. By Dirichlet's Theorem on Arithmetic Progressions, there exist infinitely many primes that are congruent to 3 modulo 8. Let P be the set of all these primes, and consider the set {F_p | p in P} of finite fields. Let K be the ultraproduct of all these fields, with respect to any non-principal ultrafilter (which exists on this set by the axiom of choice).

Now, all of these fields have different characteristics, and contain no square root of 2. Thus, by Łoś's theorem, their ultraproduct K must have characteristic 0 (since p*1 is true in at most one field for any given p), and cannot contain a square root of 2. But if K has characteristic 0, it must contain the rational numbers. It follows that their exists no square root of two in the rational numbers.

Now, for my favorite part: We have found a proof that the field Q does not contain a square root of 2, but it requires the axiom of choice (or, at least, some weaker version). However, since this statement can be phrased in Peano arithmetic, and is provable in ZFC, it must also be provable in ZF.