It so happens that I asked [an analogous question][1] at _CS Theory StackExchange_.
A brief informal summary is this.
First, it is undecidable to determine if a given theorem is provable in ZFC,
and this would not change if we knew P=NP.
Second, for other mathematical theorems (I used Goldbach's conjecture),
if P=NP, and if the theorem has a "short proof," then not only could we determine
whether the theorem is true or false, we could also find a proof quickly.
More precisely, a proof could be found "in time polynomial in the length of the statement 
and the length of the shortest proof" (to quote one respondent) using _Levin's universal search
algorithm_. 


 [1]: http://cstheory.stackexchange.com/questions/2800/if-pnp-could-we-obtain-proofs-of-goldbachs-conjecture-etc