I'm interested in formal proof verification, and one of the surprisingly difficult parts of this is dealing with proofs by contradiction. The issue is that the final step of such proofs is typically "if not P is a theorem, then false is a theorem," an inference rule in a Hilbert-like system, and Hilbert systems typically do not have "second order inference rules". To make this work, we need some version of the deduction theorem to derive "not P entails false", from which we can then derive P. This can be a pain in the neck if not done at the meta level (see http://us.metamath.org/mpegif/mmdeduction.html, for example).
Now, the deduction theorem is an admissible metatheorem; it proves that proofs exist, though the construction of the proofs is unwieldy. My question is: are there other such metatheorems (for standard first order, second order, or ZFC) whose addition is known to make proofs in Hilbert-like systems more flexible?