Theorem dmncrng

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

	Ref	Expression
Assertion	dmncrng	⊢ ( 𝑅 ∈ Dmn → 𝑅 ∈ CRingOps )

Proof

Step	Hyp	Ref	Expression
1		isdmn2	⊢ ( 𝑅 ∈ Dmn ↔ ( 𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps ) )
2	1	simprbi	⊢ ( 𝑅 ∈ Dmn → 𝑅 ∈ CRingOps )