This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnindd

Description: Principle of Mathematical Induction (inference schema) on integers, a deduction version. (Contributed by Thierry Arnoux, 19-Jul-2020)

Ref Expression
Hypotheses nnindd.1 
|- ( x = 1 -> ( ps <-> ch ) )
nnindd.2 
|- ( x = y -> ( ps <-> th ) )
nnindd.3 
|- ( x = ( y + 1 ) -> ( ps <-> ta ) )
nnindd.4 
|- ( x = A -> ( ps <-> et ) )
nnindd.5 
|- ( ph -> ch )
nnindd.6 
|- ( ( ( ph /\ y e. NN ) /\ th ) -> ta )
Assertion nnindd 
|- ( ( ph /\ A e. NN ) -> et )

Proof

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