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

Step	Hyp	Ref	Expression
1		isogrp 33062	. 2 ⊢ (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))
2	1	simplbi 497	1 ⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp)

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