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 )