Metamath Proof Explorer

Theorem dmnrngo

Description: Obsolete theorem, use idomringd instead. A domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	dmnrngo	$⊢ R \in Dmn \to R \in RingOps$

Proof

Step	Hyp	Ref	Expression
1		dmncrng	$⊢ R \in Dmn \to R \in CRingOps$
2		crngorngo	$⊢ R \in CRingOps \to R \in RingOps$
3	1 2	syl	$⊢ R \in Dmn \to R \in RingOps$