All of them. It's possible to verify if a proof is valid in polynomial time, and it's possible to check if the last step of a proof is the theorem under consideration in polynomial time, so just encode "valid proof of length N" as a satisfiability problem.
N = 1
DO
IF (there is a valid proof of length N that proves theorem T) THEN return TRUE
IF (there is a valid proof of length N that proves theorem $\lnot$ T) THEN return FALSE
N = N * 2
LOOP
Unless the theorem is unprovable, which is really just another theorem to check. A tractable SAT solver would be ridiculously powerful.
I'll try to be more explicit. A proof is a string of characters. You could ask "what is the length of your proof?" and get a response "1300 characters long". In academic papers only the outlines to proofs tend to be published, but there are proofs where every single step can be checked.
Consider an algorithm $\text{ValidProof}(P, T)$ that returns true iff $P$ is a valid proof of $T$. We already know constructively how to implement $\text{ValidProof}$ in polynomial time.
If $P=NP$, then for any algorithm $Q(x)$ which runs in polynomial time, one can solve the problem "is there $x$ of length $N$ such that $Q(x)$ is true?". You can also determine what that $x$ is. That's the entire point of the $NP$ complexity class.
Since $Q(x)$ can be $\text{ValidProof}(x, T)$, $P=NP$ would allow anyone to just solve for $x$, the proof.
