nat-indi - brismu bridi

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

Theorem nat-indi 601

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

**Hypothesis**
Ref	Expression
nat-indi.0	⊢ 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

**Assertion**
Ref	Expression
nat-indi	⊢ ro da poi ke'a kacna'u ku'o zo'u da bo'a

Distinct variable group: da , de

**Proof of Theorem nat-indi**
Step	Hyp	Ref	Expression
1		nat-indi.0	. 2 ⊢ 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
2		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
3	1, 2	ax-mp 10	1 ⊢ 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-nat-ind 600

This theorem is referenced by: nat-indii 602