This probably has been asked before, but apologies, I don't know how to locate it. I want to prove $\forall x,y: P(x, y)$. My premises are:
$$P(0, 0) \wedge \\ [\forall x: P(x, 0)] \wedge \\ [\forall y: P(0, y)] \wedge \\ [\forall x,y: P(x, y) \Rightarrow P(Suc(x), Suc(y))]$$
I can prove some basic facts in PA, such as addition is comm, assoc, etc. I can also prove things about less than, such as less than is transitive. Also, if x is less than or equal to y, then there exists a z such x + z = y. But I'm not good at induction with two variables, and so cannot complete the proof.
Here's a proof in Fitch, which has a built in Peano Induction rule:
As you can see, the only 'trick' is to just ignore the inductive hypothesis for the inside inductive proof, but instead to use the inductive hypothesis for the outside inductive proof