Metamath Proof Explorer

Theorem dmnrngo

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

Ref Expression
Assertion dmnrngo 
|- ( R e. Dmn -> R e. RingOps )

Proof

Step Hyp Ref Expression
1 dmncrng 
 |-  ( R e. Dmn -> R e. CRingOps )
2 crngorngo 
 |-  ( R e. CRingOps -> R e. RingOps )
3 1 2 syl 
 |-  ( R e. Dmn -> R e. RingOps )