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.