nat-indi - brismu bridi

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

Theorem nat-indi 595

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

This theorem was proved from axioms: ax-mp 10 ax-nat-ind 594

This theorem is referenced by: nat-indii 596