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

Theorem ogrpgrp 28026
Description: An left ordered group is a group. (Contributed by Thierry Arnoux, 9-Jul-2018.)
Assertion
Ref Expression
ogrpgrp  |-  ( G  e. oGrp  ->  G  e.  Grp )

Proof of Theorem ogrpgrp
StepHypRef Expression
1 isogrp 28025 . 2  |-  ( G  e. oGrp 
<->  ( G  e.  Grp  /\  G  e. oMnd ) )
21simplbi 458 1  |-  ( G  e. oGrp  ->  G  e.  Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1840   Grpcgrp 16267  oMndcomnd 28020  oGrpcogrp 28021
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-v 3058  df-in 3418  df-ogrp 28023
This theorem is referenced by:  ogrpinv0le  28039  ogrpsub  28040  ogrpaddlt  28041  ogrpaddltbi  28042  ogrpaddltrbid  28044  ogrpsublt  28045  ogrpinv0lt  28046  ogrpinvlt  28047  isarchi3  28064  archirng  28065  archirngz  28066  archiabllem1a  28068  archiabllem1b  28069  archiabllem1  28070  archiabllem2a  28071  archiabllem2c  28072  archiabllem2b  28073  archiabllem2  28074
  Copyright terms: Public domain W3C validator