Theorem ogrpgrp 33080

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

Syntax hints:   → wi 4   ∈ wcel 2108  Grpcgrp 18951  oMndcomnd 33074  oGrpcogrp 33075

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-ogrp 33077

This theorem is referenced by:  ogrpinv0le  33092  ogrpsub  33093  ogrpaddlt  33094  ogrpaddltbi  33095  ogrpaddltrbid  33097  ogrpsublt  33098  ogrpinv0lt  33099  ogrpinvlt  33100  isarchi3  33194  archirng  33195  archirngz  33196  archiabllem1a  33198  archiabllem1b  33199  archiabllem1  33200  archiabllem2a  33201  archiabllem2c  33202  archiabllem2b  33203  archiabllem2  33204