nat-ind-cur - brismu bridi

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

Theorem nat-ind-cur 535

Description: Curried form of ax-nat-ind 532 (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 532	. 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 ro brd 191 su'o bsd 377 ro brdp 412 kacli'e bkaclihe 517 kacna'u bkacnahu 527

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

This theorem is referenced by: (None)