Theorem ogrpgrp 31329

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

Syntax hints:   → wi 4   ∈ wcel 2106  Grpcgrp 18577  oMndcomnd 31323  oGrpcogrp 31324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ogrp 31326

This theorem is referenced by:  ogrpinv0le  31341  ogrpsub  31342  ogrpaddlt  31343  ogrpaddltbi  31344  ogrpaddltrbid  31346  ogrpsublt  31347  ogrpinv0lt  31348  ogrpinvlt  31349  isarchi3  31441  archirng  31442  archirngz  31443  archiabllem1a  31445  archiabllem1b  31446  archiabllem1  31447  archiabllem2a  31448  archiabllem2c  31449  archiabllem2b  31450  archiabllem2  31451