Theorem ogrpgrp 20256

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Grpcgrp 19061  oMndcomnd 20250  oGrpcogrp 20251

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-in 3909  df-ogrp 20253

This theorem is used by:  ogrpinv0le  20267  ogrpsub  20268  ogrpaddlt  20269  ogrpaddltbi  20270  ogrpaddltrbid  20272  ogrpsublt  20273  ogrpinv0lt  20274  ogrpinvlt  20275  isarchi3  33629  archirng  33630  archirngz  33631  archiabllem1a  33633  archiabllem1b  33634  archiabllem1  33635  archiabllem2a  33636  archiabllem2c  33637  archiabllem2b  33638  archiabllem2  33639