Theorem ogrpgrp 31981

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

Step	Hyp	Ref	Expression
1		isogrp 31980	. 2 ⊢ (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))
2	1	simplbi 498	1 ⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2106  Grpcgrp 18762  oMndcomnd 31975  oGrpcogrp 31976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ogrp 31978

This theorem is referenced by:  ogrpinv0le  31993  ogrpsub  31994  ogrpaddlt  31995  ogrpaddltbi  31996  ogrpaddltrbid  31998  ogrpsublt  31999  ogrpinv0lt  32000  ogrpinvlt  32001  isarchi3  32093  archirng  32094  archirngz  32095  archiabllem1a  32097  archiabllem1b  32098  archiabllem1  32099  archiabllem2a  32100  archiabllem2c  32101  archiabllem2b  32102  archiabllem2  32103