Is there proof by mathematical induction in which the inductive step is itself proven by mathematical induction? Mathematical induction is the proof method that shows the truth of $\forall n\in\mathbb N:P(n)$ by establishing these two things:


*

*Base case: $E(0)$,

*Inductive step: $\forall n\in\mathbb N:P(n)\implies P(n+1).$


My question is:

Is there a mathematical proof by induction that establishes the inductive step itself by mathematical induction? I.e. establishing $\forall n\in\mathbb N:P(n)\implies P(n+1)$ by showing that:
  
  
*
  
*$P(0)\implies P(1)$,
  
*$\forall n\in\mathbb N:(P(n)\implies P(n+1))\implies (P(n+1)\implies P(n+2))$
  
  
  If there are such proofs, are they just artificial or do they occur in praxis?

 A: There isn't any "natural" one.
Indeed given formulas $A,B,C$, $(A\to B)\to (B\to C)$ is equivalent to $\neg (\neg A\lor B) \lor (\neg B\lor C)$ which in turn is equivalent to $(A\land \neg B)\lor (\neg B\lor C)$, distributing over the middle $\lor$ this gives $(A\lor \neg B\lor C)\land (\neg B\lor \neg B\lor C)$ and then noting that $\neg B\lor C$ implies $A\lor \neg B\lor C$ we see that this last formula is equivalent to $\neg B\lor C$, that is $B\to C$.
According to the completeness theorem for propositional logic, this equivalence $(A\to B)\to (B\to C) \cong (B\to C)$ can be proved, and so in particular if you have a proof of $(P(n)\to P(n+1))\to (P(n+1)\to P(n+2))$, you have a proof of $P(n+1)\to P(n+2)$. 
Therefore if you know how to prove $P(0)$ and $P(0)\to P(1)$ and $\forall n, (P(n)\to P(n+1))\to (P(n+1)\to P(n+2))$, you know how to prove $P(0), P(1)$ and $\forall n\geq 1, P(n)\to P(n+1)$ using only basic properties of integers and no induction (only $n\geq 1\to \exists m, m+1= n$).Then with induction you can derive $\forall n, P(n)$.
So there is no "natural proof" that uses this scheme, although as the other answers show, it's not rare to use another induction in the induction step.
A: Yes, there are non-artificial examples.
Consider, for instance, the statement that, for every $n\in\mathbb N$,$$1^3+2^3+\cdots+n^3=(1+2+\cdots+n)^2.$$Let $n\in\mathbb N$ and suppose that the previous statement holds for that $n$. Then you want to prove that$$1^3+2^3+\cdots+(n+1)^3=\bigl(1+2+\cdots+(n+1)\bigr)^2.$$But$$1^3+2^3+\cdots+(n+1)^3=(1+2+\cdots+n)^2+(n+1)^3$$and$$\bigl(1+2+\cdots+(n+1)\bigr)^2=(1+2+\cdots+n)^2+2(1+2+\cdots+n)(n+1)+(n+1)^2.$$Now, in order to prove the equality between the right-hand sides of the latest two equalities, it is convenient to use the fact that$$1+2+\cdots+n=\frac{n(n+1)}2\text,$$and it is rather natural to prove it by induction.
A: $(P(n)⇒P(n+1))⇒(P(n+1)⇒P(n+2))$ is equivalent to $P(n+1)⇒P(n+2)$, which means that assuming $P(n)⇒P(n+1)$ doesn't really help. – Fabio Somenzi 39 mins ago
A: This would be common in proving certain propositions involving more than one variable.  For example, let us prove that for any doubly indexed sequence $a_{m,n}$ satisfying $a_{m, 0} = 1$ for all $m \in \mathbb{N}$, $a_{0, n} = 1$ for all $n \in \mathbb{N}$, and $a_{m+1, n+1} = a_{m+1, n} + a_{m, n+1} + 1$ for all $m, n \in \mathbb{N}$, then $a_{m, n} = 2 \binom{m+n}{n} - 1$ for all $m, n \in \mathbb{N}$.
We prove by induction on $m$ that for all $m \in \mathbb{N}$, we have for all $n \in \mathbb{N}$, $a_{m, n} = 2 \binom{m+n}{n} - 1$.  For the base case $m = 0$, this reduces to showing for all $n \in \mathbb{N}$, $a_{0, n} = 2 \binom{n}{n} - 1$, which is easy.
For the inductive case, the inductive hypothesis would be: (1) for all $n \in \mathbb{N}$, $a_{m, n} = 2 \binom{m+n}{n} - 1$.  What we need to prove is: for all $n \in \mathbb{N}$, $a_{m + 1, n} = 2 \binom{(m+1)+n}{n} - 1$.  We prove this by induction on $n$.  Here, the base case $n = 0$ would be $a_{m+1, 0} = 2 \binom{m+1}{0} - 1$ which again is easy.  For the inductive case, the inductive hypothesis would be: (2) $a_{m+1, n} = 2 \binom{(m+1)+n}{n} - 1$.  What we need to prove is: $a_{m+1, n+1} = 2 \binom{(m+1)+(n+1)}{n+1} - 1$.  However, we are given that $a_{m+1, n+1} = a_{m+1,n} + a_{m,n+1} + 1$.  We also know from (2) that $a_{m+1,n} = 2 \binom{m+1+n}{n} - 1$; and from a special case of (1), we know that $a_{m,n+1} = 2 \binom{m+n+1}{n} - 1$.  Therefore, $a_{m+1, n+1} = 2 \binom{m+n+1}{n} + 2 \binom{m+n+1}{n+1} - 1 = 2 \binom{m+n+2}{n+1} - 1$ by Pascal's identity.  Thus, the inner induction establishes $a_{m+1, n} = 2 \binom{m+1+n}{n} - 1$ for all $n \in \mathbb{N}$.
We have therefore proved the inductive case for the outer induction; therefore, we have shown what we wanted: forall $m \in \mathbb{N}$, forall $n \in \mathbb{N}$, $a_{m, n} = 2 \binom{m+n}{n} - 1$.
