nat-ind-cur - brismu bridi

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

Theorem nat-ind-cur 603

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

**Assertion**
Ref	Expression
nat-ind-cur	⊢ ganai li no 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 600	. 2 ⊢ ganai ge li no 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 61	1 ⊢ ganai li no 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 47 su'o bsd 416 ro brdp 469 kacli'e bkaclihe 585 kacna'u bkacnahu 595

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

This theorem is referenced by: (None)