Cut elimination shows that if a sentence is provable in first-order logic, it is provable with a particularly nice type of proof in a natural deduction system without the "cut" rule, which is essentially modus ponens in that system. In particular these proofs have the subformula property – every formula in the entire proof is a subformula of the formula being proved.
The cut elimination theorem and its generalizations are key tools in proof theory. Gentzen proved cut elimination in 1934 and used it as part of his consistency proof of Peano arithmetic; there is a nice survey article "The art of ordinal analysis" by Michael Rathjen in Proc. ICM 2006.
The cut elimination theorem can be used to give nice proofs of the Craig interpolation theorem and other theorems from logic; one exposition is Chapter 6 of "Logic for Computer Science" by Jean Gallier.
