Theorem isogrp 31356

Description: A (left-)ordered group is a group with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.)

Assertion

Ref	Expression
isogrp	⊢ (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))

Proof of Theorem isogrp

Step	Hyp	Ref	Expression
1		df-ogrp 31354	. 2 ⊢ oGrp = (Grp ∩ oMnd)
2	1	elin2 4134	1 ⊢ (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2101  Grpcgrp 18605  oMndcomnd 31351  oGrpcogrp 31352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1540  df-ex 1778  df-sb 2063  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3436  df-in 3896  df-ogrp 31354

This theorem is referenced by:  ogrpgrp  31357  ogrpinv0le  31369  ogrpsub  31370  ogrpaddlt  31371  isarchi3  31469  archirng  31470  archirngz  31471  archiabllem1a  31473  archiabllem1b  31474  archiabllem2a  31476  archiabllem2c  31477  archiabllem2b  31478  archiabl  31480  orngsqr  31531  ornglmulle  31532  orngrmulle  31533  ofldtos  31538  suborng  31542  reofld  31572  nn0omnd  31573