Theorem ogrpgrp 30754

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

Syntax hints:   → wi 4   ∈ wcel 2111  Grpcgrp 18095  oMndcomnd 30748  oGrpcogrp 30749

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ogrp 30751

This theorem is referenced by:  ogrpinv0le  30766  ogrpsub  30767  ogrpaddlt  30768  ogrpaddltbi  30769  ogrpaddltrbid  30771  ogrpsublt  30772  ogrpinv0lt  30773  ogrpinvlt  30774  isarchi3  30866  archirng  30867  archirngz  30868  archiabllem1a  30870  archiabllem1b  30871  archiabllem1  30872  archiabllem2a  30873  archiabllem2c  30874  archiabllem2b  30875  archiabllem2  30876