Theorem ogrpgrp 20194

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

Syntax hints:   → wi 4   ∈ wcel 2141  Grpcgrp 18999  oMndcomnd 20188  oGrpcogrp 20189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-in 3911  df-ogrp 20191

This theorem is referenced by:  ogrpinv0le  20205  ogrpsub  20206  ogrpaddlt  20207  ogrpaddltbi  20208  ogrpaddltrbid  20210  ogrpsublt  20211  ogrpinv0lt  20212  ogrpinvlt  20213  isarchi3  33473  archirng  33474  archirngz  33475  archiabllem1a  33477  archiabllem1b  33478  archiabllem1  33479  archiabllem2a  33480  archiabllem2c  33481  archiabllem2b  33482  archiabllem2  33483