Home 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.0ge 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-indiro da poi ke'a kacna'u ku'o zo'u da bo'a
Distinct variable group:   da , de

Proof of Theorem nat-indi
StepHypRef Expression
1 nat-indi.0 . 2ge 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 . 2ganai 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
31, 2ax-mp 10 1ro 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