An additional axiom of arithmetic

Let P_1, P_2, … P_7 be the Peano axioms. What will happen if we add

P+: P1 & P2 & … P7 & ∃x(Prf(x, ⌜P⌝) → P

Here ⌜P⌝ means the Gödel number of P, and Prf(x,y) means that x is a proof o y, or rather that x is the Gödel number of a sequence that is a proof a sentence with Gödel number y.
It seems to me that the axiom is true. For if our derivation system is sound, and it derives P then it is the case that P.