Theorem ogrpgrp 32727

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

Syntax hints:   → wi 4   ∈ wcel 2098  Grpcgrp 18863  oMndcomnd 32721  oGrpcogrp 32722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-v 3470  df-in 3950  df-ogrp 32724

This theorem is referenced by:  ogrpinv0le  32739  ogrpsub  32740  ogrpaddlt  32741  ogrpaddltbi  32742  ogrpaddltrbid  32744  ogrpsublt  32745  ogrpinv0lt  32746  ogrpinvlt  32747  isarchi3  32839  archirng  32840  archirngz  32841  archiabllem1a  32843  archiabllem1b  32844  archiabllem1  32845  archiabllem2a  32846  archiabllem2c  32847  archiabllem2b  32848  archiabllem2  32849