Metamath Proof Explorer


Theorem drnggrp

Description: A division ring is a group (closed form). (Contributed by NM, 8-Sep-2011)

Ref Expression
Assertion drnggrp ( 𝑅 ∈ DivRing → 𝑅 ∈ Grp )

Proof

Step Hyp Ref Expression
1 id ( 𝑅 ∈ DivRing → 𝑅 ∈ DivRing )
2 1 drnggrpd ( 𝑅 ∈ DivRing → 𝑅 ∈ Grp )