Theorem dmnrngo

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

	Ref	Expression
Assertion	dmnrngo	⊢ ( 𝑅 ∈ Dmn → 𝑅 ∈ RingOps )

Proof

Step	Hyp	Ref	Expression
1		dmncrng	⊢ ( 𝑅 ∈ Dmn → 𝑅 ∈ CRingOps )
2		crngorngo	⊢ ( 𝑅 ∈ CRingOps → 𝑅 ∈ RingOps )
3	1 2	syl	⊢ ( 𝑅 ∈ Dmn → 𝑅 ∈ RingOps )