Theorem cmn4d

Description: Commutative/associative law for commutative monoids. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	cmn4d.1	|- B = ( Base ` G )
	cmn4d.2	|- .+ = ( +g ` G )
	cmn4d.3	|- ( ph -> G e. CMnd )
	cmn4d.4	|- ( ph -> X e. B )
	cmn4d.5	|- ( ph -> Y e. B )
	cmn4d.6	|- ( ph -> Z e. B )
	cmn4d.7	|- ( ph -> W e. B )
Assertion	cmn4d	|- ( ph -> ( ( X .+ Y ) .+ ( Z .+ W ) ) = ( ( X .+ Z ) .+ ( Y .+ W ) ) )

Proof

Step	Hyp	Ref	Expression
1		cmn4d.1	|- B = ( Base ` G )
2		cmn4d.2	|- .+ = ( +g ` G )
3		cmn4d.3	|- ( ph -> G e. CMnd )
4		cmn4d.4	|- ( ph -> X e. B )
5		cmn4d.5	|- ( ph -> Y e. B )
6		cmn4d.6	|- ( ph -> Z e. B )
7		cmn4d.7	|- ( ph -> W e. B )
8	1 2	cmn4	|- ( ( G e. CMnd /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .+ ( Z .+ W ) ) = ( ( X .+ Z ) .+ ( Y .+ W ) ) )
9	3 4 5 6 7 8	syl122anc	|- ( ph -> ( ( X .+ Y ) .+ ( Z .+ W ) ) = ( ( X .+ Z ) .+ ( Y .+ W ) ) )