![]() |
brismu bridi |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > Home > Th. List > nat-indi |
Description: Inference form of ax-nat-ind 594 (Contributed by la korvo, 10-Aug-2023.) |
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 |
Ref | Expression |
---|---|
nat-indi | ⊢ ro da poi ke'a kacna'u ku'o zo'u da bo'a |
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 |
Copyright terms: Public domain | W3C validator |