Theorem ogrpgrp 30706

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

Syntax hints:   → wi 4   ∈ wcel 2114  Grpcgrp 18105  oMndcomnd 30700  oGrpcogrp 30701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ogrp 30703

This theorem is referenced by:  ogrpinv0le  30718  ogrpsub  30719  ogrpaddlt  30720  ogrpaddltbi  30721  ogrpaddltrbid  30723  ogrpsublt  30724  ogrpinv0lt  30725  ogrpinvlt  30726  isarchi3  30818  archirng  30819  archirngz  30820  archiabllem1a  30822  archiabllem1b  30823  archiabllem1  30824  archiabllem2a  30825  archiabllem2c  30826  archiabllem2b  30827  archiabllem2  30828