Metamath Proof Explorer

Theorem dmncrng

Description: A domain is a commutative ring. (Contributed by Jeff Madsen, 6-Jan-2011)

Ref Expression
Assertion dmncrng 
|- ( R e. Dmn -> R e. CRingOps )

Proof

Step Hyp Ref Expression
1 isdmn2 
 |-  ( R e. Dmn <-> ( R e. PrRing /\ R e. CRingOps ) )
2 1 simprbi 
 |-  ( R e. Dmn -> R e. CRingOps )