nat-ind-cur - brismu bridi

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

Theorem nat-ind-cur 597

Description: Curried form of ax-nat-ind 594 (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 594	. 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 414 ro brdp 463 kacli'e bkaclihe 579 kacna'u bkacnahu 589

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

This theorem is referenced by: (None)