nat-ind-cur - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > nat-ind-cur

Theorem nat-ind-cur 539

Description: Curried form of ax-nat-ind 536 (Contributed by la korvo, 20-Aug-2023.)

**Assertion**
Ref	Expression
nat-ind-cur	⊢ ganai li 0 bo'a gi ganai ro da poi ke'a bo'a ku'o zo'u su'o de zo'u ge da kacli'e de gi de bo'a gi ro da poi ke'a kacna'u ku'o zo'u da bo'a

Distinct variable group: da ,de

**Proof of Theorem nat-ind-cur**
Step	Hyp	Ref	Expression
1		ax-nat-ind 536	. 2 ⊢ ganai ge li 0 bo'a gi ro da poi ke'a bo'a ku'o zo'u su'o de zo'u ge da kacli'e de gi de bo'a gi ro da poi ke'a kacna'u ku'o zo'u da bo'a
2	1	uncur 54	1 ⊢ ganai li 0 bo'a gi ganai ro da poi ke'a bo'a ku'o zo'u su'o de zo'u ge da kacli'e de gi de bo'a gi ro da poi ke'a kacna'u ku'o zo'u da bo'a

Colors of variables: sumti selbri bridi

Syntax hints: tsb 1 btb 3 ge bge 42 su'o bsd 377 ro brdp 411 kacli'e bkaclihe 521 kacna'u bkacnahu 531

This theorem was proved from axioms: ax-mp 10 ax-k 11 ax-s 15 ax-ge-in 45 ax-nat-ind 536

This theorem is referenced by: (None)