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

Step	Hyp	Ref	Expression
1		isogrp 28025	. 2 |- ( G e. oGrp <-> ( G e. Grp /\ G e. oMnd ) )
2	1	simplbi 458	1 |- ( G e. oGrp -> G e. Grp )

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