We argue that there is a class of widely used and readily formalizable arithmetical proofs of universal properties which are not accounted for in the traditional unprovability of consistency analysis. On this basis, we offer a mathematical proof of consistency for Peano Arithmetic PA and demonstrate that this proof is formalizable in PA. This refutes the wide spread belief that there exists no consistency proof of a system that can be formalized in the system itself. Gödel’s Second Incompleteness theorem yields that PA cannot derive the consistency formula ConPA. This does not interfere with our formalized proof of PA-consistency which is not a derivation of the consistency formula ConPA.