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
(where $x^\prime$ is the successor to $x$).
From these two axioms, am I allowed to call the following theorems?
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).