There is a Fourier analytic proof for Sperner's theorem which is much more complicated than the combinatorial proof (and give less in certain respects). This was part pf the polymath1 project.

A general point is that sometime trying to prove a Theorem X using method Y is valuable even if the proof is much more complicated than needed. So while simplification of complicated proofs is a noble endeavor, complicafication of simple theorems is also not without merit!

Here is another example (taken from lecture notes by Spencer): Suppose you want to prove that there is always a 1-1 function from a (finite) set |A| to a set |B| when |B|>=|A|. But you want to prove it using the probabilistic method. Write |A|=n. If |B| is larger than n^2 or so you can show that a 1-1 map exist by considering a random function and applying the union bound. If |B| is larger than 6n or so you can apply the much more sophisticated Lovasz Local Lemma to get a proof. I am not aware of probabilistic proofs of this nature which works when |B| is smaller and this is an interesting challenge.