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

Theorem ogrpgrp 29677
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 29676 . 2 (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))
21simplbi 476 1 (𝐺 ∈ oGrp → 𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  Grpcgrp 17403  oMndcomnd 29671  oGrpcogrp 29672
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-in 3574  df-ogrp 29674
This theorem is referenced by:  ogrpinv0le  29690  ogrpsub  29691  ogrpaddlt  29692  ogrpaddltbi  29693  ogrpaddltrbid  29695  ogrpsublt  29696  ogrpinv0lt  29697  ogrpinvlt  29698  isarchi3  29715  archirng  29716  archirngz  29717  archiabllem1a  29719  archiabllem1b  29720  archiabllem1  29721  archiabllem2a  29722  archiabllem2c  29723  archiabllem2b  29724  archiabllem2  29725
  Copyright terms: Public domain W3C validator