Theorem domnring

Description: A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015)

	Ref	Expression
Assertion	domnring	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		domnnzr	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{NzRing}$$
2		nzrring	$$⊢R\in \mathrm{NzRing}\to R\in \mathrm{Ring}$$
3	1 2	syl	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{Ring}$$