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 )