Theorem ogrpgrp 33024

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

Syntax hints:   → wi 4   ∈ wcel 2109  Grpcgrp 18872  oMndcomnd 33018  oGrpcogrp 33019

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924  df-ogrp 33021

This theorem is referenced by:  ogrpinv0le  33036  ogrpsub  33037  ogrpaddlt  33038  ogrpaddltbi  33039  ogrpaddltrbid  33041  ogrpsublt  33042  ogrpinv0lt  33043  ogrpinvlt  33044  isarchi3  33148  archirng  33149  archirngz  33150  archiabllem1a  33152  archiabllem1b  33153  archiabllem1  33154  archiabllem2a  33155  archiabllem2c  33156  archiabllem2b  33157  archiabllem2  33158