Theorem crngorngo

Description: A commutative ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Assertion	crngorngo	$$⊢R\in \mathrm{CRingOps}\to R\in \mathrm{RingOps}$$

Proof

Step	Hyp	Ref	Expression
1		iscrngo	$$⊢R\in \mathrm{CRingOps}\leftrightarrow \left(R\in \mathrm{RingOps}\wedge R\in \mathrm{Com2}\right)$$
2	1	simplbi	$$⊢R\in \mathrm{CRingOps}\to R\in \mathrm{RingOps}$$