Proving ZFC results using large cardinals There are many $ZFC$ results that their proof uses forcing: The idea is that we force the statement to be true, and then using absoluteness (or other reasons) we conclude that the result is true in $ZFC$.
Question. Are there any $ZFC$ results such that in their proof we use large cardinals (and then remove the use of that large cardinal by some arguments like absoluteness)?
 A: Shelah's original argument for $CON(\mathfrak{a}>\mathfrak{d})$ assumes the existence of measurable cardinal, an assumption which is later eliminated in order to obtain a ZFC result.
The paper can be found here: http://arxiv.org/pdf/math/0012170.pdf
A: A famous result of Jensen is the coding theorem showing that the universe can be extended by class forcing to a model of the form $L[a]$, with $a$ a real, in a way that the original ground model can be decoded from $a$. (Jensen's result is stronger than this.)
The argument is delicate even if $0^\sharp$ does not exist (in this case, other proofs are known, also involved. One is due to Shelah and Stanley). 
The published proof appeared in the book Coding the universe by Beller, Jensen, and Welch; there are reworkings and extensions, for example by Friedman, but maintaining the same outline. It presents two different arguments, depending on whether $0^\sharp$ exists (the division is needed mainly because of the covering lemma). 
(To be fair, as Mohammad indicates in a comment, Sy has a proof that does not require this splitting. Also, Sy has extensions of the result, where we are interested not just in the coding but also in preserving non-trivial large cardinal structure present in the universe. His latest advance in this direction is at the level of Woodin cardinals, see Genericity and Large Cardinals, Journal of Mathematical Logic, Vol. 5, No. 2, pp. 149-166, 2005.)
This is not exactly what you are asking, but I believe it is as close as we can get: A proof that splits in cases according to whether certain large cardinal assumption holds or not, requiring a different approach in either case.
A: If rather than large cardinals we concentrate on their consistency strength, a source of examples comes from applications of forcing axioms. 
A notorious case is Justin Moore's result that there is a basis of order $5$ for the uncountable linear orders if $\mathsf{PFA}$ holds. The result is essentially a consequence of his Mapping reflection principle $\mathsf{MRP}$. Careful analysis of the proof reveals that the full strength of $\mathsf{MRP}$ is not required, and as a consequence this strength has been reduced considerably, showing that the same holds in a forcing extension of $L$, requiring only rather mild large cardinals. This appeared in joint work by König, Larson, Moore, and Velickovic.
A slightly different situation is the following: Todorcevic established that $\mathsf{PFA}$ implies Kaplansky's conjecture. He also showed several strong partition relations on $\omega_1$ from the same assumption. Analysis of the proofs shows that the proper posets responsible for these results can be defined in $\mathsf{ZFC}$. The situation is different from the case above in that it was clear from the beginning that $\mathsf{PFA}$ or large cardinals were not needed (other than for clarity of to provide an easy to quote context for the results). In the same spirit, many applications of $\mathsf{MRP}$ to combinatorics on $\omega_1$ are equiconsistent with $\mathsf{ZFC}$. Large cardinal strength is needed once one attempts the analogous results at the level of $\omega_2$ or larger.
A: I am not sure if this is a sort of example you asked for but it seems interesting so I will mention it. There are several ZFC results that are proved in the following way: You assume the result does not hold and that gives you a highly saturated ideal (over a small large cardinal which Fremlin calls quasi measurable). Then you force with this ideal, form the well founded generic ultrapower in the extension and argue towards a contradiction. An example of such a theorem is: For every sequence $\{X_n : n < \omega\}$ of subsets of $[0, 1]$ there is a disjoint refinement of full outer measure, i.e., there is a sequence $\{Y_n : n < \omega\}$ of pairwise disjoint sets such that $Y_n \subseteq X_n$ and $X_n$ and $Y_n$ have same (Lebesgue) outer measure. This is due to Gitik and Shelah. Another such application is: For every $X \subseteq [0, 1]$, there is a $Y \subseteq X$, such that $X$ and $Y$ have same outer measure and the distance between any two points of $Y$ is irrational - So $Y$ is Vitali like inside $X$ and it has full outer measure.
