Are there any good nonconstructive "existential metatheorems"?

Eh, this is more of an "existential meta-algorithm," but I think it's perhaps worth mentioning...

One consequence of the Robertson-Seymour graph minor theorem is that for any given surface, there's a polynomial-time algorithm (actually cubic time!) to decide if a graph can be drawn on that surface. But this algorithm isn't explicit -- since it relies on testing a finite but not effectively bounded number of graphs to see whether they're minors of the input graph. Actually, as far as I know we can't even describe this algorithm for checking if a graph is embeddable on a torus -- and computing the graph genus in general is known to be NP-complete! So we know that an "efficient" algorithm exists, although describing it is known (assuming P \neq NP) to be hard.

Set theory provides a good example. It is often convenient in set theory to work with the concept of "classes" and treat them as mathematical objects of their own kind. The standard axiomatization of set theory with classes is called Goedel-Bernays set theory, denoted GBC, whereas the usual ZFC axioms have only set objects. But there is a general theorem that any statement purely about sets that is proved by using classes in GBC can be proved without them purely in ZFC. This is what it means to say that GBC is a conservative extension of ZFC. To prove this general theorem, it suffices to observe that any ZFC model can be expanded to a model of GBC, by adding only the classes definable from parameters.

There are many other examples of conservative extensions in mathematics, and all of them would seem to be examples of the type that you seek. For example, PA has a conservative extension to the analogous theory true in the collection HF of hereditarily finite sets. Thus, to prove a theorem about numbers in PA, one can freely use heredtiarily finite sets (e.g. sequences of numbers, sequences of sets of numbers, etc.), not just as coded by numbers via Goedel coding, but as actual mathematical objects. And surely this makes proofs much easier.

Perhaps another type of example arises in the absoluteness phenomenon in set theory. For example, the Shoenfield Absoluteness theorem states that any Sigma^1_2 statement has the same truth value in any two models of set theory with the same ordinals. In particular, to prove that a particular Sigma^1_2 statement is true in ZFC, it suffices to prove it under the assumption also that V=L, where one also has all kinds of additional structure available. The Absoluteness Theorems (and there are many) can therefore be viewed under the rubric you mention.

But of course, in all these cases, we have an actual proof in the weaker theory. To prove that there is a proof, is a proof, so I believe ultimately there will be no way to avoid the quibbling over whether it is easy or hard to translate the high-level proof into a low level proof, since in principle it will always be possible to do this.

Harvey Friedman has an example of a finite statement (that's actually "finite" and not "finitary," i.e., $\Pi_0^0$ rather than $\Pi^0_1$) that has a proof, using large cardinal axioms, that is no more than a million symbols in length, but whose proof in ZFC with abbreviations must contain more than $10^{1000}$ symbols. Obviously, explicitly "finding" the ZFC proof is totally infeasible. See the last theorem (Theorem 5) in this post to the Foundations of Mathematics mailing list.

In some sense, computational infeasibility is the only kind of obstruction that can exist here. If there is a proof then you can find it by exhaustive search, so there cannot be a nonconstructive argument for the existence of a proof in the strong sense of an argument that gives you no algorithm whatsoever for finding the proof. Thus by some measure, Friedman's example is about the strongest kind of example you could hope for.