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 30735
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 30734 . 2 (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))
21simplbi 501 1 (𝐺 ∈ oGrp → 𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  Grpcgrp 18094  oMndcomnd 30729  oGrpcogrp 30730
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-v 3471  df-in 3915  df-ogrp 30732
This theorem is referenced by:  ogrpinv0le  30747  ogrpsub  30748  ogrpaddlt  30749  ogrpaddltbi  30750  ogrpaddltrbid  30752  ogrpsublt  30753  ogrpinv0lt  30754  ogrpinvlt  30755  isarchi3  30847  archirng  30848  archirngz  30849  archiabllem1a  30851  archiabllem1b  30852  archiabllem1  30853  archiabllem2a  30854  archiabllem2c  30855  archiabllem2b  30856  archiabllem2  30857
  Copyright terms: Public domain W3C validator