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

Metamath Proof Explorer

Theorem crngmgp

Description: A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015)

		Ref	Expression
	Hypothesis	ringmgp.g	$⊢ G = {mulGrp}_{R}$
	Assertion	crngmgp	$⊢ R \in CRing \to G \in CMnd$

Step	Hyp	Ref	Expression
1		ringmgp.g	$⊢ G = {mulGrp}_{R}$
2	1	iscrng	$⊢ R \in CRing \leftrightarrow (R \in Ring \land G \in CMnd)$
3	2	simprbi	$⊢ R \in CRing \to G \in CMnd$