Metamath Proof Explorer


Theorem nn0indd

Description: Principle of Mathematical Induction (inference schema) on nonnegative integers, a deduction version. (Contributed by Thierry Arnoux, 23-Mar-2018)

Ref Expression
Hypotheses nn0indd.1 x=0ψχ
nn0indd.2 x=yψθ
nn0indd.3 x=y+1ψτ
nn0indd.4 x=Aψη
nn0indd.5 φχ
nn0indd.6 φy0θτ
Assertion nn0indd φA0η

Proof

Step Hyp Ref Expression
1 nn0indd.1 x=0ψχ
2 nn0indd.2 x=yψθ
3 nn0indd.3 x=y+1ψτ
4 nn0indd.4 x=Aψη
5 nn0indd.5 φχ
6 nn0indd.6 φy0θτ
7 1 imbi2d x=0φψφχ
8 2 imbi2d x=yφψφθ
9 3 imbi2d x=y+1φψφτ
10 4 imbi2d x=Aφψφη
11 6 ex φy0θτ
12 11 expcom y0φθτ
13 12 a2d y0φθφτ
14 7 8 9 10 5 13 nn0ind A0φη
15 14 impcom φA0η