Theorem ogrpgrp 30037

Description: An 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 30036	. 2 ⊢ (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))
2	1	simplbi 479	1 ⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2144  Grpcgrp 17629  oMndcomnd 30031  oGrpcogrp 30032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-in 3728  df-ogrp 30034

This theorem is referenced by:  ogrpinv0le  30050  ogrpsub  30051  ogrpaddlt  30052  ogrpaddltbi  30053  ogrpaddltrbid  30055  ogrpsublt  30056  ogrpinv0lt  30057  ogrpinvlt  30058  isarchi3  30075  archirng  30076  archirngz  30077  archiabllem1a  30079  archiabllem1b  30080  archiabllem1  30081  archiabllem2a  30082  archiabllem2c  30083  archiabllem2b  30084  archiabllem2  30085