It is often mentioned the main use of forcing is to prove independence facts, but it also seems a way to prove theorems. For instance how would one try to prove Erdös-Rado, $\beth_n^{+} \to (\aleph_1)_{\aleph_0}^{n+1}$ (or in particular that $(2^{\aleph_0})^+ \to (\aleph_1)_{\aleph_0}^2$) by using forcing? Is it simpler than the combinatorial proof? Which partial order would one use?
Or can one try to show that forcing the negation of the Erdös-Rado is impossible or inconsistent?
I never heard anyone claim the existence of a forcing proof of the Erdős-Rado theorem. On the other hand, yes, there are several proofs of nonindependence statements that use forcing. One is Shelah's proof for the existence of a finite K4-free graph which, when the edges colored by 2 colors, always contains a monocolored triangle (a problem of Erdős and Hajnal). Here is the argument. He constructs a forcing extension which adds a graph X with the same property but with ℵ0 colors (this is not easy). Obviously, X has the edge-coloring property for 2 colors, as well. X must contain a finite subgraph Y with the same property. This is compactness, or, any proof for the Erdős-de Bruijn theorem gives it. As forcing cannot create new finite graphs, Y is already present in the underlying model. That is, there is a finite graph as required in any countable, transitive model of a sufficiently large part of ZFC. By Gödel, this is only possible, if ZFC proves that there is such a graph.
Another example is the original proof of the Baumgartner-Hajnal theorem: ω1→(α)2k if α<ω1, k<ω. They first deduced it from Martin's axiom, then a specific argument gives that if it holds in a cardinal preserving extension, then it holds in the original model. Therefore, it holds in every countable, transitive model of a sufficiently large fragment of ZFC, and we can finish as above.
The situation isn't that any given theorem off the shelf might have a forcing proof, but rather that it is a fascinating situation when one can use forcing to prove a theorem purely about the ground model. For such proofs, one makes a conclusion about the set-theoretic universe $V$ by first going to another universe $V[G]$, and then by analyzing the relationship between $V$ and $V[G]$, making a conclusion purely about $V$.
Let me illustrate with a few concrete examples.
There are incomparable Turing degrees. This theorem is usually proved by a combinatorial constructive argument, meeting infinitely many requirements in sequence. However, there is also a soft forcing proof: add two mutually generic Cohen reals $c$ and $d$. By genericity, neither is computable from the other, and so the assertion is true in $V[c][d]$. But the assertion there are incomparable degrees has complexity $\Sigma^1_1$, and hence is absolute to $V$. So the statement is true in $V$, as desired.
A similar argument produces an infinite antichain this way, with the further property that any real computable from two of them is outright computable with no oracle. Similarly, one can make conclusions about hyperarithmetic incomparability this way, with a very soft argument essentially without any hyperarithmetic details.
Indeed, many constructions in computability theory can be viewed as forcing arguments in this way. Rather than describing a detailed construction meeting certain requirements at certain stages, one shows that the requirements correspond to dense sets in a certain partial order and then appeals to genericity. One could use actual genericity and then absoluteness to claim that the desired objects already exist in the ground model, as I did above, or alternatively just note that there were only countably many dense sets to meet and thus the objects exist by the usual diagonalization.
Another example arises in Borel equivalence relation theory, in the result that there is no Borel reduction of $E_0$, the relation of almost-equality on binary sequences, to equality. The classical proof uses ergodic theory, but there is a quick forcing argument. Suppose it did reduce; this fact is absolute to the forcing $V[c]$ adding a Cohen real. Since any finite change in $c$ is still generic, the particular real $w$ that $c$ maps to under the reduction does not depend on $c$, and hence is in the ground model $V$. But the assertion that some real maps to $w$ is absolute, and so $c$ differs finitely from a ground model real, contradiction.
Similar forcing arguments yield other non-reductions in Borel equivalence relation theory. For exmple, the relation $E_{set}$ can be treated by the forcing $Coll(\omega,\mathbb{R})$, since any two generic reals for this partial order enumerate the same set, the set of ground model reals.
I think there are numerous examples of ZFC theorems proved via forcing, and I would encourage you to edit your question to explicitly encourage people to post such answers, as I would be very interested to see additional such examples. In this case, the big-list tag might be appropriate.
One way to use forcing to prove actual ZFC results is by using absoluteness. I do not know of a forcing proof of Erdös-Rado, but there is a forcing proof of the somewhat similar Baumgartner-Hajnal theorem that $\omega_1\rightarrow(\alpha)^2_2$ for any countable ordinal $\alpha<\omega_1$. The only absoluteness fact you need for this is that if $M\subseteq N$ are transitive models of ZFC and $T$ is a tree in $M$, then $T$ is well-founded in $M$ if and only if it is well-founded in $N$.
In outline the proof of Baumgartner-Hajnal is as follows. First it is shown that Martin's Axiom (MA) implies the partition relation $\omega_1\rightarrow(\alpha)^2_2$. Now show that it holds in an arbitrary countable transitive model $M$ of ZFC. Given a coloring $\chi:[\omega_1]^2\rightarrow 2$ in $M$ we seek a $\chi$-homogeneous set of ordertype $\alpha$ in $M$. Use a ccc forcing to extend $M$ to a transitive model $N$ with the same cardinals and satisfying MA. Since $N$ satisfies MA it contains a $\chi$-homogeneous set of ordertype $\alpha$. Then define a tree (in $M$) of finite approximations to such a homogeneous set, so that a branch through the tree corresponds exactly to such a homogeneous set. Since the tree is not well-founded in $N$, it is also not well-founded in $M$ and so we get our homogeneous set in $M$.
This theorem first appeared in the paper by Baumgartner and Hajnal "A proof (involving Martin's axiom) of a partition relation" Fund. Math., 78(3):193–203, 1973 and you can get it here: http://matwbn.icm.edu.pl/ksiazki/fm/fm78/fm78121.pdf
This is not an answer to your question about the Erdos-Rado theorem, but a remark concerning another example of a forcing proof of a ZFC result (a result which is actually quite useful and observed by several authors). For every infnite subset $L$ of $\mathbb{N}$ denote by $[L]^{\infty}$ the set of all infinite subsets of $L$.
Let $X$ be a Polish space and $A$ be a co-analytic subset of $[\mathbb{N}]^{\infty}\times X$ such that for every $L\in [\mathbb{N}]^{\infty}$ there exists $x\in X$ with $(L,x)in A$. Then there exist an infinite subset $M$ of $\mathbb{N}$ and a continuous map $f:[M]^{\infty}\to X$ such that $(N,f(N))\in A$ for every $N\in [M]^{\infty}$.
The result can be easily proved under MA. It is also easily seen to be absolute, therefore it is true in ZFC. Nevertheless, to the best of my knowledge, no "classical" proof is known.
There is also a theorem saying that a sequence of canonical Borel approximations of an analytic non-Borel set from inside can never be of a bounded Borel rank
There are also some model-theoretic examples of such proofs (in ZFC). Once you prove that for a given logic L, the notions of consistency and completeness (for theories in L) are absolute, it's possible to prove (in ZFC) the existence of some interesting models (described by an L-theory) just by showing that such models exist in some generic extension. One example is presented in a paper by Shelah called "Nonstandard uniserial module over a uniserial domain exists", the proof uses a completeness theorem for stationary logic.
An example from elementary geometry is the very simple forcing argument to establish the non-axiomatizability (in infinitary logic) of Sperner spaces, due to Blass and Pambuccian: Blass, A.; Pambuccian, V. "Sperner spaces and first order logic." Mathematical Logic Quarterly vol. 49, no. 2 (March, 2003), 111-114. The proof uses a cardinal collapse and absoluteness.
One use of forcing as a tool to prove theorems that has not been mentioned in the answers is the method of generic ultrapowers, where we take an ideal $I$ on an uncountable regular cardinal $\kappa$ (in the sense of $M$), and consider the poset $P,\leq$ of those subsets of $\kappa$ that has positive measure (the ordering is by subset). A generic filter $F$ of that poset will end up being an $M$-ultrafilter in $M[G]$, which extends the filter dual to $I$. And if $I$ is {$\kappa$-complete, normal} in $M$, $G$ will be {$\kappa$-complete, normal}.
If $I$ indeed has the requisite properties, then in $M[G]$ we can form the ultrapower of $M$ by $G$, and an elementary embedding $j:V\to Ult(M,G)$. This way, we allow ourselves the liberty of "pretending" to have an elementary embedding $j:V\to M$ without being necessarily committed to the existence of large cardinals.
The generic ultrapower is not necessarily well-founded (an ideal is precipitous (which, incidentally, means příkrý in Czech) iff the generic ultrapower obtained is well-founded). But having such a construction at hand can be useful. Example 22.15 in Jech illustrates one such use.
Theorem. Let $\kappa$ be a singular cardinal of uncountable cofinality, and assume GCH holds below $\kappa$, then $2^\kappa=\kappa^+$.
The proof is to use the nonstationary ideal on $(cf(\kappa))^M$, then in the extension we obtain a normal $M$-measure on $(cf(\kappa))^M$, which we use to construct the ultrapower. One key observation is that the poset of positive measure subsets will have size $2^{cf(\kappa)}<\kappa$, so its cc property implies that cardinals above $\kappa$ are preserved. By studying the combinatorial properties of objects in $Ult$, we may infer that $(|\mathcal{P}^M(\kappa)|)^{M[G]}\leq(\kappa^+)^{M[G]}$, which can be transferred back to $M$ because of the observation.
Matthew Wiener once explained to me that because of the close connections between forcing and the Baire category theorem, forcing could be used to prove certain results in analysis that are more commonly proved via BCT. Unfortunately, all I've been able to find is this article where Wiener sketches a proof via forcing of the existence of continuous nowhere-differentiable functions of Hausdorff dimension one. Perhaps some other MO reader can supply the missing details.
