This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmncrng

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

		Ref	Expression
	Assertion	dmncrng	$⊢ R \in Dmn \to R \in CRingOps$

Step	Hyp	Ref	Expression
1		isdmn2	$⊢ R \in Dmn \leftrightarrow (R \in PrRing \land R \in CRingOps)$
2	1	simprbi	$⊢ R \in Dmn \to R \in CRingOps$