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

Metamath Proof Explorer

Theorem crngring

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

		Ref	Expression
	Assertion	crngring	$⊢ R \in CRing \to R \in Ring$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
2	1	iscrng	$⊢ R \in CRing \leftrightarrow (R \in Ring \land {mulGrp}_{R} \in CMnd)$
3	2	simplbi	$⊢ R \in CRing \to R \in Ring$