For example, Skolemizations (and the dual operation of Herbrandization) are used, proof-theoretically, when one wants "reductions" of first order logic to propositional logic. 

 1. In order to prove the consistency of a first order theory finitarily, one can consider, by Skolemization, a conservative open extension of the theory. If this extension is simple enough, then one can use Hilbert-Ackermann consistency theorem, which says that an open theory $T$ is inconsistent iff there is a disjunction of negations of instances of the axioms of $T$ that is a tautological consequence of axioms of identity. For example, consider Robinson Arithmetic $Q$. One Standard formulation of $Q$ is not open: it has an axiom saying that if $n$ is not zero then there exists a predecessor of $n$. The Skolemization of this axiom introduces the symbol of the predecessor function, and now we can replace the original axiom by an open one. Now, it is easy to define a (propositional) valuation, based on the usual algorithms for the arithmetic functions, and this shows that the condition in the Hilbert-Ackermann theorem cannot hold. Notice that, the Hilbert-Ackermann theorem itself is a reduction to first-order to propositional logic that was first proved (finitarily) by use of epsilon-operator, which is almost the same thing as Skolemization. 

 2. Herbrand Theorem: a more complete reduction of first-order logic to propositional logic. It says that a sentence in prenex normal form is a logical theorem iff there is a disjunction of instances of the matrix of the Herbrand normal form of the sentence (the midsequent) that is tautological consequence of instances of equality axioms. The (finitary) proof of this theorem can be done in two steps: first, prove the theorem for existential sentences in prenex normal form, and, after that, show that an arbitrary sentence is equivalent for validity to its Herbrandization. The technique of Skolemization is used throughout in this proof: the existential case is essentially Hilbert-Ackerman, and the Herbrandization is dual to Skolemization. 

 3. Any proof of the completeness theorem for first order logic must, at some point, deal with the validation of existential sentences. This proof can be done by Skolemization, through a reduction of the general case to the case in which the theory is open. In the case the theory is open, the proof of the completeness can be done more simply, because now you do't have to worry about the validity of existentials in the canonical structure. There is an (easy) exercise in Shoenfield's book dedicated to this proof. The proof uses only propositional concepts, such as "tautologically complete set of quantifier free sentences" and the construction of the canonical structure. This is another reduction of first order to propositional logic.

 4. Also, the reduction of first order to propositional logic can be useful in decidability problems. For example, the set of valid existential sentences that contains no function symbols (but may contain constants) is decidable. This can be proved finitarily, by use of Herbrand's theorem: it is decidable whether a quantifier free formula is tautological consequence of instances of equality axioms in a language without function symbols. In fact, if the quantifier free, function symbol free formula $\varphi$ is a tautological consequence of equality axioms $A_1$,..., $A_n$ then, identifying all variables and constants of $\varphi$ and $A_1$,..., $A_n$ with $x$, it follows that $\varphi*$ is a tautological consequence of equality axioms $A^*_1$,..., $A^*_n$, where  $\varphi*$ and $A^*_1$,..., $A^*_n$ are the resulting formulas with all terms identified with $x$. It is easy to see that all new equality axioms (the $A^*_i$) can be dropped, possibly with the exception of the equality axiom $x=x$. Now, it is decidable if $\varphi*$ is a tautological consequence of $x=x$. The infinitary proof of this fact is based on the remark that $\varphi$ is valid iff it is valid in all finite models of a specific (finite) cardinality.

In general, the infinitary proofs of the finitary results mentioned above are easy.