![]() |
brismu bridi |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > Home > Th. List > nat-indii |
Description: Inference form of ax-nat-ind 594 (Contributed by la korvo, 10-Aug-2023.) |
Ref | Expression |
---|---|
nat-indii.0 | ⊢ li no bo'a |
nat-indii.1 | ⊢ 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 |
Ref | Expression |
---|---|
nat-indii | ⊢ ro da poi ke'a kacna'u ku'o zo'u da bo'a |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nat-indii.0 | . . 3 ⊢ li no bo'a | |
2 | nat-indii.1 | . . 3 ⊢ 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 | |
3 | 1, 2 | ge-ini 55 | . 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 |
4 | 3 | nat-indi 595 | 1 ⊢ ro da poi ke'a kacna'u ku'o zo'u da bo'a |
Colors of variables: sumti selbri bridi |
Syntax hints: btb 3 ge bge 47 su'o bsd 414 ro brdp 463 kacli'e bkaclihe 579 |
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) |
Copyright terms: Public domain | W3C validator |