Theorem crngring

Description: A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Assertion	crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
2	1	iscrng	⊢ ( 𝑅 ∈ CRing ↔ ( 𝑅 ∈ Ring ∧ ( mulGrp ‘ 𝑅 ) ∈ CMnd ) )
3	2	simplbi	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )