This is very much an intuitionist statement, i.e., it's obvious that 7 is prime.
A formalist, however, goes to great pains to prove that 7 is prime using no more than his axiom set. On the way he incidently defines 7, defines multiplication, and in the process also finds that multiplication commutes. The 7's primeness and multiplication's commutivity have equal standing.
Kronecker might have been the consummate intuitionist in stating that only integers are obvious. He also argued that infinity must be excluded from mathematics. But since he couldn't do much useful mathematics from those positions he blithely used all manner of "non-intuitionist" notions in his serious work. It was all a matter of not allowing his philosophy to interfere with his industry.
Just because I say that objective mathematical truth exists, it doesn't mean that I think that formalism is unnecessary. On the contrary, formalism is the means by which we get at mathematical truth, so the limitations of formalism cannot be avoided. But regardless, our theorems "touch" things that exist independently of our choices of description.
It's like the difference between a description of the Rock of Gibraltar and the Rock itself. I can write about it in a hundred different languages, and some of the things I say in one language won't even make sense when translated into another. Now a formalist comes along and points out that the letters that I put onto paper are a shifting sand: many readings are possible even for a given statement, and not all are equivalent, despite my pains to make the descriptions as accurate as possible. Perhaps he even concludes on the basis of this that the Rock doesn't exist.
My answer is that the descriptions aren't the Rock itself. I can't get the Rock onto paper. But nevertheless the Rock has an objective existence that is independent of whatever I write about it, and the statements do refer to it. Insofar as the statements are correct in the context of their own languages, the statements reflect the properties of the Rock.
A formalist, however, goes to great pains to prove that 7 is prime using no more than his axiom set.
Fair enough, perhaps that was a bad example. Here's another: Gödel's theorem. It's different from the primality of seven, because it doesn't assume a formal system. It is a statement about all possible formal systems. It goes beyond formalism; it's true before I even pick an axiom set. Here's another (related) example: the universality of computation.