brismu bridi |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > Home > Th. List > ga-com-lem |
Description: Lemma for ga-com 147 (Contributed by la korvo, 31-Jul-2023.) |
Ref | Expression |
---|---|
ga-com-lem | ⊢ ganai ga broda gi brode gi ga brode gi broda |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ga-rin 143 | . 2 ⊢ ganai broda gi ga brode gi broda | |
2 | ga-lin 142 | . 2 ⊢ ganai brode gi ga brode gi broda | |
3 | 1, 2 | garii 144 | 1 ⊢ ganai ga broda gi brode gi ga brode gi broda |
Colors of variables: sumti selbri bridi |
Syntax hints: ga bga 137 |
This theorem was proved from axioms: ax-mp 10 ax-k 11 ax-s 15 ax-ge-le 43 ax-ge-re 44 ax-ge-in 45 |
This theorem depends on definitions: df-go 61 df-ga 138 |
This theorem is referenced by: ga-com 147 |
Copyright terms: Public domain | W3C validator |