Theorem domnring

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

	Ref	Expression
Assertion	domnring	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		domnnzr	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
2		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
3	1 2	syl	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )