Nested induction In a statement involving two universal quantifiers, a way of proving is by proceeding with nested induction, I.e. proving inductively the first quantification such that in each part of the induction, we have another induction for the second quantification. My question is the following: in the induction step of the outer induction, may I use the induction hypothesis of the outer one in the induction step of the inner induction, thus effectively using two induction steps?
 A: The argument for double induction/nested induction is:
$$\begin{array}{|l}\text{In the domain of }\Bbb N^+\\\hdashline 1\quad P(1,1)\\2\quad \forall m\geq 1:P(m,1)\to P(m+1,1)\\3\quad \forall m\geq 1,\forall n\geq 1: P(m,n)\to P(m, n+1) \\ \hline 4 \quad  \forall m\geq 1: P(m,1)\qquad\qquad\qquad\qquad\quad\text{Induction from 1,2}\\ \quad\begin{array}{|l}~\quad[k]\quad k\geq 1\\\hline5\quad P(k,1)\qquad\qquad\qquad\qquad\qquad\qquad\text{Universal Instantiation from 4}\\6\quad \forall n\geq 1:P(k,n)\to P(k, n+1)\quad~~~\text{Universal Instantiation from 3}\\7\quad\forall n\geq 1: P(k,n)\qquad\qquad\qquad\qquad\text{Induction from 5,6} \end{array}\\8\quad \forall m\geq 1, \forall n\geq 1: P(m,n)\qquad\qquad\quad~\text{Universal Generalisation from 7} \end{array}$$
So, your task is to justify the premises 1,2,3, so that you can use the argument to justify the conclusion 8.   In practice it is sufficient to justify premises 1 and 2, and step 6 (for any aritrary $k$).


My question is the following: in the induction step of the outer induction, may I use the induction hypothesis of the outer one in the induction step of the inner induction, thus effectively using two induction steps?

If you can, then you may.   However, if you cannot, then you mustnot. 
When any justification for $\forall m\geq 1~\forall n\geq 1: P(m,n)\to P(m,n+1)$ could also be a justification for $\forall n\geq 1~\forall m\geq 1: P(m,n)\to P(m+1,n)$, due to symmetry, then you will be justifing premises 2 and 3 simultaneously.
A: Let me outline a double induction proof.  We want to prove $\forall m \forall n P(m,n)$ where the domain of discourse is the positive integers.  As basis, we prove $\forall m P(m, 1).$  Now we assume for some $n,$ $$\forall m P(m,n)\tag 1.$$  Now $(1)$ is our induction hypothesis.  I guess is is what you call the "inner induction hypothesis."  So we have to prove, $$\forall m P(m,n+1)\tag 2.$$  If we can prove $(2)$ then we are done, by induction.  We can prove $(2)$ however we choose (so long as the proof is correct) including proving it by induction.  This would make our proof a double induction.  (I've never heard the term "nested induction" before, but it's clear that you mean the same thing as I mean by "double induction.)
Now of course you can use $(1)$ in the proof of $(2).$  That's the whole idea of indiction.  So yes, you can have two induction hypotheses at the same time.  I'm a bit confused as to whether this is using the "the induction hypothesis of the outer one in the induction step of the inner induction"  or the other way around, but it doesn't really matter. 
