Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ogrpgrp Structured version   Visualization version   GIF version

Theorem ogrpgrp 30037
 Description: An left ordered group is a group. (Contributed by Thierry Arnoux, 9-Jul-2018.)
Assertion
Ref Expression
ogrpgrp (𝐺 ∈ oGrp → 𝐺 ∈ Grp)

Proof of Theorem ogrpgrp
StepHypRef Expression
1 isogrp 30036 . 2 (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))
21simplbi 479 1 (𝐺 ∈ oGrp → 𝐺 ∈ Grp)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2144  Grpcgrp 17629  oMndcomnd 30031  oGrpcogrp 30032 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-in 3728  df-ogrp 30034 This theorem is referenced by:  ogrpinv0le  30050  ogrpsub  30051  ogrpaddlt  30052  ogrpaddltbi  30053  ogrpaddltrbid  30055  ogrpsublt  30056  ogrpinv0lt  30057  ogrpinvlt  30058  isarchi3  30075  archirng  30076  archirngz  30077  archiabllem1a  30079  archiabllem1b  30080  archiabllem1  30081  archiabllem2a  30082  archiabllem2c  30083  archiabllem2b  30084  archiabllem2  30085
 Copyright terms: Public domain W3C validator