Theorem indstrd

Description: Strong induction, deduction version. (Contributed by Steven Nguyen, 13-Jul-2025)

	Ref	Expression
Hypotheses	indstrd.1	|- ( x = y -> ( ps <-> ch ) )
	indstrd.2	|- ( x = A -> ( ps <-> th ) )
	indstrd.3	|- ( ( ph /\ x e. NN /\ A. y e. NN ( y < x -> ch ) ) -> ps )
	indstrd.4	|- ( ph -> A e. NN )
Assertion	indstrd	|- ( ph -> th )

Proof

Step	Hyp	Ref	Expression
1		indstrd.1	|- ( x = y -> ( ps <-> ch ) )
2		indstrd.2	|- ( x = A -> ( ps <-> th ) )
3		indstrd.3	|- ( ( ph /\ x e. NN /\ A. y e. NN ( y < x -> ch ) ) -> ps )
4		indstrd.4	|- ( ph -> A e. NN )
5		eleq1	|- ( x = A -> ( x e. NN <-> A e. NN ) )
6	5 2	imbi12d	|- ( x = A -> ( ( x e. NN -> ps ) <-> ( A e. NN -> th ) ) )
7	6	adantl	|- ( ( ph /\ x = A ) -> ( ( x e. NN -> ps ) <-> ( A e. NN -> th ) ) )
8	1	imbi2d	|- ( x = y -> ( ( ph -> ps ) <-> ( ph -> ch ) ) )
9		bi2.04	|- ( ( y < x -> ( ph -> ch ) ) <-> ( ph -> ( y < x -> ch ) ) )
10	9	ralbii	|- ( A. y e. NN ( y < x -> ( ph -> ch ) ) <-> A. y e. NN ( ph -> ( y < x -> ch ) ) )
11		r19.21v	|- ( A. y e. NN ( ph -> ( y < x -> ch ) ) <-> ( ph -> A. y e. NN ( y < x -> ch ) ) )
12	10 11	bitri	|- ( A. y e. NN ( y < x -> ( ph -> ch ) ) <-> ( ph -> A. y e. NN ( y < x -> ch ) ) )
13	3	3com12	|- ( ( x e. NN /\ ph /\ A. y e. NN ( y < x -> ch ) ) -> ps )
14	13	3exp	|- ( x e. NN -> ( ph -> ( A. y e. NN ( y < x -> ch ) -> ps ) ) )
15	14	a2d	|- ( x e. NN -> ( ( ph -> A. y e. NN ( y < x -> ch ) ) -> ( ph -> ps ) ) )
16	12 15	biimtrid	|- ( x e. NN -> ( A. y e. NN ( y < x -> ( ph -> ch ) ) -> ( ph -> ps ) ) )
17	8 16	indstr	|- ( x e. NN -> ( ph -> ps ) )
18	17	com12	|- ( ph -> ( x e. NN -> ps ) )
19	4 7 18	vtocld	|- ( ph -> ( A e. NN -> th ) )
20	4 19	mpd	|- ( ph -> th )