Am I allowed to substitute terms when reasoning in Peano Arithmetic?

Question

I feel a little silly asking this question, but here goes. I'm on Chapter 1 of "Forcing for Mathematicians" by Nik Weaver and doing some of the exercises.

When doing stuff in Peano Arithmetic, can I substitute in terms? For example, axioms 3 and 4 of the "non-logical axioms" (as enumerated in the book) are:

(3) $x+0=x$ and

(4) $x+y^\prime=(x+y)^\prime$

(where $x^\prime$ is the successor to $x$).

From these two axioms, am I allowed to call the following theorems?

$(x+0)+y^\prime=((x+0)+y)^\prime$

$(x+0)+y^\prime=(x+y)^\prime$

$x+y'=((x+0)+y)$'

It feels right that I should be able to, but I don't see any axiom that allows this (and their are other axioms that seem to handle these kinds of "obvious" things such a one related to the renaming of variables).

Answer 1

Yes, substitution is allowed as an axion of first-order logic, nothing wrong here.

Answer 2

Yes. If you want axioms to cite, see the equality-defining axioms (2-5 here).