I wonder whether 'deepness' is subjective or not. The Compactness Theorem of first-order logic has several proofs.
Theorem. (Gödel-Maltsev) Given a language $L$ and a set $S$ of first-order sentences in that language, if every finite subset of $S$ has a model, then $S$ has model.
(For one immediate application, one can deduce in a straightforewared way that there is an infinite field containing the field $\bf R$ of real numbers, containing infinitesimal/infinite elements and having the same first order properties as $\bf R$)
Some Proofs. (I believe there are many more)
(1) Gödel's original proof (for Gödel, in 1929, this Theorem was stated as a 'Remark') is from his Completeness Theorem, stated in the particular case where the language $L$ is countable. The proof does not use the axiom of choice. Hard for me to say the nature of the proof. Grammatical maybe.
(2) I don't know precisely the nature of Maltsev's proof, published in German in 1936, and extending G.'s result to the case of an arbitrary signature $L$, using the axiom of choice.
(3) Los' proof via the 'explicit' construction of the model as ultraproduct of finite structures, using the 'axiom of the ultrafilter', which is weaker that the axiom of choice. I would say this proof is of a topological nature.
In the same (?) vein, Gromov's 'bounded version' of his Theorem stating that a finitely generated group of polynomial growth as a nilpotent subgroup of finite index has several (at least 2) proofs, apparently.
Theorem. (Gromov) For any positive integers $k$, $d$, $n$, there exists a positive integer $m$ such that any $n$-generated group, in which for all $r= 1,\dots,m$ the size of the ball of radius $r$ centered at the identity is at most $kr^d$, has a subgroup of index and nilpotency class at most $m$.
I read that Gromov's original proof is a Compactness argument. Van den Dries and Wilkie gave an alternative proof using Gödel's Compactness Theorem. Belegradek recently provided a third proof using yet another kind of compactness argument, using very little model theory.