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	|- .x. = ( .r ` R )
	crngcomd.r	|- ( ph -> R e. CRing )
	crngcomd.1	|- ( ph -> X e. B )
	crngcomd.2	|- ( ph -> Y e. B )
Assertion	crngcomd	|- ( ph -> ( X .x. Y ) = ( Y .x. X ) )

Proof

Step	Hyp	Ref	Expression
1		crngcomd.b	|- B = ( Base ` R )
2		crngcomd.t	|- .x. = ( .r ` R )
3		crngcomd.r	|- ( ph -> R e. CRing )
4		crngcomd.1	|- ( ph -> X e. B )
5		crngcomd.2	|- ( ph -> Y e. B )
6	1 2	crngcom	|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( X .x. Y ) = ( Y .x. X ) )
7	3 4 5 6	syl3anc	|- ( ph -> ( X .x. Y ) = ( Y .x. X ) )