If you are willing to consider completeness of fragments of first-order logic, one example that would follow under your scheme is the conservativity of classical logic over its [fragment of coherent logic][1]. Before the proof of [Barr's theorem][2] (1974), which settles this conservativity result, the way to see it was via [Deligne's completeness theorem][3] from SGA IV (1972) stating that a coherent topos has enough points. This is essentially a completeness theorem for coherent logic with respect to (set-valued) models. Therefore, if there is a proof in classical logic of a coherent sequent $\sigma$ from a set of coherent axioms $\mathbb{T}$, by soundness it is true in all set models, and therefore the completeness of coherent logic implies that it must be provable already in the coherent fragment. 

However explicit transformations of classical proofs of the coherent sequent from coherent axioms into proofs in the coherent fragment were not obtained until later. One of them is given in Palmgren, E.: "An intuitionistic axiomatisation of real closed fields" (2002) by using the Dragalin-Friedman translation. Another is in Sara Negri's "Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem" (2003) where the transformation follows from cut elimination. (Negri uses the word "geometric" to mean "coherent").


  [1]: https://ncatlab.org/nlab/show/coherent+logic
  [2]: https://ncatlab.org/nlab/show/Barr%27s+theorem
  [3]: https://ncatlab.org/nlab/show/Deligne+completeness+theorem