Theorem ogrpgrp 29703

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 29702	. 2 |- ( G e. oGrp <-> ( G e. Grp /\ G e. oMnd ) )
2	1	simplbi 476	1 |- ( G e. oGrp -> G e. Grp )

Syntax hints:   -> wi 4   e. wcel 1990   Grpcgrp 17422  oMndcomnd 29697  oGrpcogrp 29698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ogrp 29700

This theorem is referenced by:  ogrpinv0le  29716  ogrpsub  29717  ogrpaddlt  29718  ogrpaddltbi  29719  ogrpaddltrbid  29721  ogrpsublt  29722  ogrpinv0lt  29723  ogrpinvlt  29724  isarchi3  29741  archirng  29742  archirngz  29743  archiabllem1a  29745  archiabllem1b  29746  archiabllem1  29747  archiabllem2a  29748  archiabllem2c  29749  archiabllem2b  29750  archiabllem2  29751