Theorem ogrpgrp 20340

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Grpcgrp 19145  oMndcomnd 20334  oGrpcogrp 20335

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4091  df-ogrp 20337

This theorem is used by:  ogrpinv0le  20351  ogrpsub  20352  ogrpaddlt  20353  ogrpaddltbi  20354  ogrpaddltrbid  20356  ogrpsublt  20357  ogrpinv0lt  20358  ogrpinvlt  20359  isarchi3  33791  archirng  33792  archirngz  33793  archiabllem1a  33795  archiabllem1b  33796  archiabllem1  33797  archiabllem2a  33798  archiabllem2c  33799  archiabllem2b  33800  archiabllem2  33801