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

Metamath Proof Explorer

Theorem crngcomd

Description: Multiplication is commutative in a commutative ring. (Contributed by SN, 8-Mar-2025)

	Ref	Expression
Hypotheses	crngcomd.b	$⊢ B = {Base}_{R}$
	crngcomd.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	crngcomd.r	$⊢ φ \to R \in CRing$
	crngcomd.1	$⊢ φ \to X \in B$
	crngcomd.2	$⊢ φ \to Y \in B$
Assertion	crngcomd	$⊢ φ \to X \underset{˙}{\cdot} Y = Y \underset{˙}{\cdot} X$

Step	Hyp	Ref	Expression
1		crngcomd.b	$⊢ B = {Base}_{R}$
2		crngcomd.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		crngcomd.r	$⊢ φ \to R \in CRing$
4		crngcomd.1	$⊢ φ \to X \in B$
5		crngcomd.2	$⊢ φ \to Y \in B$
6	1 2	crngcom	$⊢ (R \in CRing \land X \in B \land Y \in B) \to X \underset{˙}{\cdot} Y = Y \underset{˙}{\cdot} X$
7	3 4 5 6	syl3anc	$⊢ φ \to X \underset{˙}{\cdot} Y = Y \underset{˙}{\cdot} X$