Theorem ogrpgrp 20301

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Grpcgrp 19106  oMndcomnd 20295  oGrpcogrp 20296

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3905  df-ogrp 20298

This theorem is used by:  ogrpinv0le  20312  ogrpsub  20313  ogrpaddlt  20314  ogrpaddltbi  20315  ogrpaddltrbid  20317  ogrpsublt  20318  ogrpinv0lt  20319  ogrpinvlt  20320  isarchi3  33682  archirng  33683  archirngz  33684  archiabllem1a  33686  archiabllem1b  33687  archiabllem1  33688  archiabllem2a  33689  archiabllem2c  33690  archiabllem2b  33691  archiabllem2  33692