Theorem ogrpgrp 20137

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

Syntax hints:   → wi 4   ∈ wcel 2132  Grpcgrp 18947  oMndcomnd 20131  oGrpcogrp 20132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-v 3446  df-in 3902  df-ogrp 20134

This theorem is referenced by:  ogrpinv0le  20148  ogrpsub  20149  ogrpaddlt  20150  ogrpaddltbi  20151  ogrpaddltrbid  20153  ogrpsublt  20154  ogrpinv0lt  20155  ogrpinvlt  20156  isarchi3  33317  archirng  33318  archirngz  33319  archiabllem1a  33321  archiabllem1b  33322  archiabllem1  33323  archiabllem2a  33324  archiabllem2c  33325  archiabllem2b  33326  archiabllem2  33327