Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ogrpgrp Structured version   Visualization version   GIF version

Theorem ogrpgrp 33080
Description: A left-ordered group is a group. (Contributed by Thierry Arnoux, 9-Jul-2018.)
Assertion
Ref Expression
ogrpgrp (𝐺 ∈ oGrp → 𝐺 ∈ Grp)

Proof of Theorem ogrpgrp
StepHypRef Expression
1 isogrp 33079 . 2 (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))
21simplbi 497 1 (𝐺 ∈ oGrp → 𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  Grpcgrp 18951  oMndcomnd 33074  oGrpcogrp 33075
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-ogrp 33077
This theorem is referenced by:  ogrpinv0le  33092  ogrpsub  33093  ogrpaddlt  33094  ogrpaddltbi  33095  ogrpaddltrbid  33097  ogrpsublt  33098  ogrpinv0lt  33099  ogrpinvlt  33100  isarchi3  33194  archirng  33195  archirngz  33196  archiabllem1a  33198  archiabllem1b  33199  archiabllem1  33200  archiabllem2a  33201  archiabllem2c  33202  archiabllem2b  33203  archiabllem2  33204
  Copyright terms: Public domain W3C validator