Prove that a statement or its negation follows from ZFC There are several problems which have been shown to be unprovable in ZFC. Has there ever been a case of the opposite? That is, has it ever been proven for some statement $\varphi$ that $\text{ZFC} \models \varphi$ or $\text{ZFC} \models \neg \varphi$, without actually proving which one is true? If not, would it make sense for a proof like this to exist or is it unlikely that something like this will ever happen?
edit: As mentioned by the two answers I was not clear enough what I am looking for. I meant a statement for which it was not clear at first whether it is unprovable but then it was shown that a proof or disproof exists, without immediately finding it. The particular statement which causes me to think about this is P=NP.
 A: It is easy to see that ZFC either proves or disproves
$$ \sin\left(10^{10^{100}}\right) > 0 $$
but we have no idea whether one or the other is the case.
This may seem like cheating, in that finding out whether it is provable or not is just a matter of computing a googol digits of $\pi$ and reducing. However all examples will have more or less this property. As soon as we know that either $\varphi$ or $\neg\varphi$ is provable, we can in principle find out which is the case in finite time, just by enumerating all proofs from ZFC until we hit one that concludes either $\varphi$ or $\neg\varphi$.
A: This question is not well-formulated as it stands. I will give you a trivial example of such a formula:
$$402439 \times 284665 = 114560397935.$$
It is clear for general reasons, that ZFC either proves this true or proves it false. However, I feel it is safe to say that it is not currently known which of these cases holds.
You will of course - quite reasonably - object that there exists an algorithm that determines which case holds. 
However, more generally, this will always be the case in your situation. The algorithm to determine which of $\varphi$ and $\lnot \varphi$ is provable is simply to start systematically writing down all possible proofs in ZFC. Eventually, one of the two formulas $\varphi$ or $\lnot \varphi$ will come up, and at that point you'll have your answer.
Now it is true that there is a gulf, in terms of computation time, between the two examples I've presented. But what do you make of this?
(1) The game of chess is winnable for White.
Nobody knows a proof of this (or its negation), but it is clear that with enough computation time, we could get the answer. Would you put this in the category of questions about simple arithmetic, or the category of more difficult questions? 
My point has been to illustrate that, given a particular $\varphi$, a meaningful answer to your question will generally involve reference to the computation time it would take to answer which of $\varphi$ or $\lnot \varphi$ is provable.
Edit. To respond to the last part of the question, Goldbach's weak conjecture, that every odd integer greater than or equal to $7$ is the sum of three primes, was proved in 2013 by Helfgott. In 1937, Vinogradov had proved this true for all odd integers greater than some constant $C$, and around 1947, an explicit, but enormous, value for $C$ was found. So between 1947 and 2013, it was clear that the weak conjecture was either provable or disprovable, but it wasn't known which one.
