Theorem ogrpgrp

Description: A left-ordered group is a group. (Contributed by Thierry Arnoux, 9-Jul-2018)

	Ref	Expression
Assertion	ogrpgrp	⊢ ( 𝐺 ∈ oGrp → 𝐺 ∈ Grp )

Proof

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