FOM: P vs NP and Peano Arithmetic

[Stephen Fenner]

I remember there being a theorem along these lines:

If  PA + (all true Pi^0_1 sentences) does not prove P!=NP, then there is a
deterministic algorithm for SAT that runs in time n^{f(n)}, where f(n)
grows more slowly than any PA-provably recursive function.

Presumably this also holds with PA replaced with any sufficiently strong
theory.  Does anybody know a reference for this result?

Steve