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 -> ( ps <-> ch ) )
nn0indd.2
|- ( x = y -> ( ps <-> th ) )
nn0indd.3
|- ( x = ( y + 1 ) -> ( ps <-> ta ) )
nn0indd.4
|- ( x = A -> ( ps <-> et ) )
nn0indd.5
|- ( ph -> ch )
nn0indd.6
|- ( ( ( ph /\ y e. NN0 ) /\ th ) -> ta )
Assertion nn0indd
|- ( ( ph /\ A e. NN0 ) -> et )

Proof

Step Hyp Ref Expression
1 nn0indd.1
 |-  ( x = 0 -> ( ps <-> ch ) )
2 nn0indd.2
 |-  ( x = y -> ( ps <-> th ) )
3 nn0indd.3
 |-  ( x = ( y + 1 ) -> ( ps <-> ta ) )
4 nn0indd.4
 |-  ( x = A -> ( ps <-> et ) )
5 nn0indd.5
 |-  ( ph -> ch )
6 nn0indd.6
 |-  ( ( ( ph /\ y e. NN0 ) /\ th ) -> ta )
7 1 imbi2d
 |-  ( x = 0 -> ( ( ph -> ps ) <-> ( ph -> ch ) ) )
8 2 imbi2d
 |-  ( x = y -> ( ( ph -> ps ) <-> ( ph -> th ) ) )
9 3 imbi2d
 |-  ( x = ( y + 1 ) -> ( ( ph -> ps ) <-> ( ph -> ta ) ) )
10 4 imbi2d
 |-  ( x = A -> ( ( ph -> ps ) <-> ( ph -> et ) ) )
11 6 ex
 |-  ( ( ph /\ y e. NN0 ) -> ( th -> ta ) )
12 11 expcom
 |-  ( y e. NN0 -> ( ph -> ( th -> ta ) ) )
13 12 a2d
 |-  ( y e. NN0 -> ( ( ph -> th ) -> ( ph -> ta ) ) )
14 7 8 9 10 5 13 nn0ind
 |-  ( A e. NN0 -> ( ph -> et ) )
15 14 impcom
 |-  ( ( ph /\ A e. NN0 ) -> et )