![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > ogrpgrp | Structured version Visualization version GIF version |
Description: A left-ordered group is a group. (Contributed by Thierry Arnoux, 9-Jul-2018.) |
Ref | Expression |
---|---|
ogrpgrp | ⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isogrp 33062 | . 2 ⊢ (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd)) | |
2 | 1 | simplbi 497 | 1 ⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 Grpcgrp 18964 oMndcomnd 33057 oGrpcogrp 33058 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-in 3970 df-ogrp 33060 |
This theorem is referenced by: ogrpinv0le 33075 ogrpsub 33076 ogrpaddlt 33077 ogrpaddltbi 33078 ogrpaddltrbid 33080 ogrpsublt 33081 ogrpinv0lt 33082 ogrpinvlt 33083 isarchi3 33177 archirng 33178 archirngz 33179 archiabllem1a 33181 archiabllem1b 33182 archiabllem1 33183 archiabllem2a 33184 archiabllem2c 33185 archiabllem2b 33186 archiabllem2 33187 |
Copyright terms: Public domain | W3C validator |