Theorem ogrpgrp 20201

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  Grpcgrp 19006  oMndcomnd 20195  oGrpcogrp 20196

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911  df-ogrp 20198

This theorem is used by:  ogrpinv0le  20212  ogrpsub  20213  ogrpaddlt  20214  ogrpaddltbi  20215  ogrpaddltrbid  20217  ogrpsublt  20218  ogrpinv0lt  20219  ogrpinvlt  20220  isarchi3  33516  archirng  33517  archirngz  33518  archiabllem1a  33520  archiabllem1b  33521  archiabllem1  33522  archiabllem2a  33523  archiabllem2c  33524  archiabllem2b  33525  archiabllem2  33526