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

Metamath Proof Explorer

Theorem dmnrngo

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

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

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$