Home brismu bridi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  exlimdh

Theorem exlimdh 425
Description: Deduction converting universal quantification to existential quantification. (Contributed by la korvo, 9-Jul-2025.)
Hypotheses
Ref Expression
exlimdh.0ganai broda gi ro da zo'u broda
exlimdh.1ganai brodi gi ro da zo'u brodi
exlimdh.2ganai broda gi ganai brode gi brodi
Assertion
Ref Expression
exlimdhganai broda gi ganai su'o da zo'u brode gi brodi

Proof of Theorem exlimdh
StepHypRef Expression
1 exlimdh.0 . . 3ganai broda gi ro da zo'u broda
2 exlimdh.2 . . 3ganai broda gi ganai brode gi brodi
31, 2alrimih 238 . 2ganai broda gi ro da zo'u ganai brode gi brodi
4 exlimdh.1 . . 3ganai brodi gi ro da zo'u brodi
54eqih 422 . 2go ro da zo'u ganai brode gi brodi gi ganai su'o da zo'u brode gi brodi
63, 5sylib 105 1ganai broda gi ganai su'o da zo'u brode gi brodi
Colors of variables: sumti selbri bridi
Syntax hints:   ganai bgan 9   ro brd 222   su'o bsd 414
This theorem was proved from axioms:  ax-mp 10  ax-k 11  ax-s 15  ax-ge-le 48  ax-gen1 224  ax-qi1 234  ax-eq 420
This theorem depends on definitions:  df-go 83
This theorem is referenced by:  exim  426
  Copyright terms: Public domain W3C validator