It depends on what your axiom system is, what 0 is, and what your universe is. In Peano arithmetic it's axiomatic. Meanwhile, for fields (and possibly less-structred rings) in abstract algebra, it's a theorem. An important note is that the proof for fields requires negative numbers, while Peano arithmetic only describes the natural numbers.

Here's the field proof I'm pulling out of memeory:

  x*0 = x*(y + -y) = x*y + x*(-y) = x*y - x*y = 0

This relies on the existence of additive inverses for the first step, distribution in the second step, and the fact that x(-y) = -(xy) in the third step. That third property can be derived from sufficiently-specific ring axioms, but I forget how specific they have to be. It might be true in any ring by virtue of distribution but I forget the proof.

So to answer your question, yes there are... but it depends on the context. In some situations it may need to be axiomatic. A recursively-defined system like Peano may need to take it axiomatically as a base case.