"The complete proof of 2 + 2 = 4 involves 2,863 subtheorems including the 189 above. (The command "show trace_back 2p2e4 /essential" will list them.) These have a total of 27,426 steps—this is how many steps you would have to examine if you wanted to verify the proof by hand in complete detail all the way back to the axioms." http://us.metamath.org/mpegif/mmset.html#trivia

For example, consider a rather trivial theorem which says that if you have two positive integers in decimal representations Aaa...aa and Bbb..bb, of same length, then the sum of them is larger than number (A+B)00..00.

So this theorem gives you a property of the result (the result is larger than some number) without you having to calculate the result (sum the numbers) explicitly.

The Hashlife algorithm mentioned in this thread is another case, basically it's an algorithm to prove certain "theorems" about the Game of Life and applying those theorems to speed it up.