Theorem mndass

Description: A monoid operation is associative. (Contributed by NM, 14-Aug-2011) (Proof shortened by AV, 8-Feb-2020)

	Ref	Expression
Hypotheses	mndcl.b	|- B = ( Base ` G )
	mndcl.p	|- .+ = ( +g ` G )
Assertion	mndass	|- ( ( G e. Mnd /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )

Proof

Step	Hyp	Ref	Expression
1		mndcl.b	|- B = ( Base ` G )
2		mndcl.p	|- .+ = ( +g ` G )
3		mndsgrp	|- ( G e. Mnd -> G e. Smgrp )
4	1 2	sgrpass	|- ( ( G e. Smgrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )
5	3 4	sylan	|- ( ( G e. Mnd /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )