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 33063
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
StepHypRef Expression
1 isogrp 33062 . 2 (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))
21simplbi 497 1 (𝐺 ∈ oGrp → 𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  Grpcgrp 18964  oMndcomnd 33057  oGrpcogrp 33058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-in 3970  df-ogrp 33060
This theorem is referenced by:  ogrpinv0le  33075  ogrpsub  33076  ogrpaddlt  33077  ogrpaddltbi  33078  ogrpaddltrbid  33080  ogrpsublt  33081  ogrpinv0lt  33082  ogrpinvlt  33083  isarchi3  33177  archirng  33178  archirngz  33179  archiabllem1a  33181  archiabllem1b  33182  archiabllem1  33183  archiabllem2a  33184  archiabllem2c  33185  archiabllem2b  33186  archiabllem2  33187
  Copyright terms: Public domain W3C validator