brismu bridi |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > Home > Th. List > hbth |
Description: Hypothesis builder: theorems are closed. (Contributed by la korvo, 25-Jun-2024.) |
Ref | Expression |
---|---|
hbth.0 | ⊢ broda |
Ref | Expression |
---|---|
hbth | ⊢ ganai broda gi ro da zo'u broda |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbth.0 | . . 3 ⊢ broda | |
2 | 1 | ax-gen1 179 | . 2 ⊢ ro da zo'u broda |
3 | 2 | ki 12 | 1 ⊢ ganai broda gi ro da zo'u broda |
Colors of variables: sumti selbri bridi |
Syntax hints: ro brd 177 |
This theorem was proved from axioms: ax-mp 10 ax-k 11 ax-gen1 179 |
This theorem is referenced by: nfth 363 |
Copyright terms: Public domain | W3C validator |