Theorem ogrpgrp 20175

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 20174	. 2 ⊢ (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))
2	1	simplbi 500	1 ⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2143  Grpcgrp 18985  oMndcomnd 20169  oGrpcogrp 20170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-ogrp 20172

This theorem is referenced by:  ogrpinv0le  20186  ogrpsub  20187  ogrpaddlt  20188  ogrpaddltbi  20189  ogrpaddltrbid  20191  ogrpsublt  20192  ogrpinv0lt  20193  ogrpinvlt  20194  isarchi3  33373  archirng  33374  archirngz  33375  archiabllem1a  33377  archiabllem1b  33378  archiabllem1  33379  archiabllem2a  33380  archiabllem2c  33381  archiabllem2b  33382  archiabllem2  33383