I think that two good examples are the Cartan-Kähler Existence Theorem and the Cartan-Kuranishi Prolongation Theorem.

The first theorem gives sufficient (but quite subtle) conditions for a system of (real-analytic) PDE (possibly overdetermined or with degenerate symbol) to be locally solvable and describes the 'generality' of the generic real-analytic solution. Its simplest case (which is still not trivial to prove) is the Cauchy-Kowalewskaya Theorem.

The second theorem says that, under certain technical conditions that are not easy to state without a lot of preparation and definitions (but that are almost always satisfied in practice), a specific algorithm for replacing a given system of real-analytic PDE by an equivalent system of PDE (i.e., one that has the same real-analytic solutions) will, after a finite number of applications, yield either a system that satisfies the sufficient conditions of the Cartan-Kähler Theorem or a system that is formally incompatible (and hence has no real-analytic solutions).

Cartan used the first theorem many times in his work to derive some rather surprising results, and it continues to yield surprising and interesting results today in differential geometry and PDE, many very far from anything suggested by the statement of the theorem. Cartan assumed the second theorem was true (it was not until after Cartan's death that Kuranishi actually proved it) and didn't exactly use it so much as rely on its truth to motivate many of his calculations. (The second theorem has, since then, been used directly in various classification theorems, etc.)