nat-ind-cur - brismu bridi

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

Theorem nat-ind-cur 537

Description: Curried form of ax-nat-ind 534 (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 534	. 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 411 kacli'e bkaclihe 519 kacna'u bkacnahu 529

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

This theorem is referenced by: (None)