Metamath Proof Explorer


Theorem nnsinds

Description: Strong (or "total") induction principle over the naturals. (Contributed by Scott Fenton, 16-May-2014)

Ref Expression
Hypotheses nnsinds.1 x = y φ ψ
nnsinds.2 x = N φ χ
nnsinds.3 x y 1 x 1 ψ φ
Assertion nnsinds N χ

Proof

Step Hyp Ref Expression
1 nnsinds.1 x = y φ ψ
2 nnsinds.2 x = N φ χ
3 nnsinds.3 x y 1 x 1 ψ φ
4 elnnuz N N 1
5 elnnuz x x 1
6 5 3 sylbir x 1 y 1 x 1 ψ φ
7 1 2 6 uzsinds N 1 χ
8 4 7 sylbi N χ