Theorem ogrpgrp 20095

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

Syntax hints:   → wi 4   ∈ wcel 2121  Grpcgrp 18904  oMndcomnd 20089  oGrpcogrp 20090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-in 3892  df-ogrp 20092

This theorem is referenced by:  ogrpinv0le  20106  ogrpsub  20107  ogrpaddlt  20108  ogrpaddltbi  20109  ogrpaddltrbid  20111  ogrpsublt  20112  ogrpinv0lt  20113  ogrpinvlt  20114  isarchi3  33272  archirng  33273  archirngz  33274  archiabllem1a  33276  archiabllem1b  33277  archiabllem1  33278  archiabllem2a  33279  archiabllem2c  33280  archiabllem2b  33281  archiabllem2  33282