Metamath Proof Explorer

Theorem ogrpgrp

Description: A left-ordered group is a group. (Contributed by Thierry Arnoux, 9-Jul-2018)

Ref Expression
Assertion ogrpgrp 
|- ( G e. oGrp -> G e. Grp )

Proof

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