![]() |
brismu bridi |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > Home > Th. List > exlimdh |
Description: Deduction converting universal quantification to existential quantification. (Contributed by la korvo, 9-Jul-2025.) |
Ref | Expression |
---|---|
exlimdh.0 | ⊢ ganai broda gi ro da zo'u broda |
exlimdh.1 | ⊢ ganai brodi gi ro da zo'u brodi |
exlimdh.2 | ⊢ ganai broda gi ganai brode gi brodi |
Ref | Expression |
---|---|
exlimdh | ⊢ ganai broda gi ganai su'o da zo'u brode gi brodi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimdh.0 | . . 3 ⊢ ganai broda gi ro da zo'u broda | |
2 | exlimdh.2 | . . 3 ⊢ ganai broda gi ganai brode gi brodi | |
3 | 1, 2 | alrimih 238 | . 2 ⊢ ganai broda gi ro da zo'u ganai brode gi brodi |
4 | exlimdh.1 | . . 3 ⊢ ganai brodi gi ro da zo'u brodi | |
5 | 4 | eqih 422 | . 2 ⊢ go ro da zo'u ganai brode gi brodi gi ganai su'o da zo'u brode gi brodi |
6 | 3, 5 | sylib 105 | 1 ⊢ ganai 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 |