Theorem mndassd

Description: A monoid operation is associative. (Contributed by Thierry Arnoux, 3-Aug-2025)

	Ref	Expression
Hypotheses	mndassd.1	$$⊢B={\mathrm{Base}}_G$$
	mndassd.2	$$⊢\underset{\dot{}}{+}={+}_G$$
	mndassd.3	$$⊢\phi \to G\in \mathrm{Mnd}$$
	mndassd.4	$$⊢\phi \to X\in B$$
	mndassd.5	$$⊢\phi \to Y\in B$$
	mndassd.6	$$⊢\phi \to Z\in B$$
Assertion	mndassd	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		mndassd.1	$$⊢B={\mathrm{Base}}_G$$
2		mndassd.2	$$⊢\underset{\dot{}}{+}={+}_G$$
3		mndassd.3	$$⊢\phi \to G\in \mathrm{Mnd}$$
4		mndassd.4	$$⊢\phi \to X\in B$$
5		mndassd.5	$$⊢\phi \to Y\in B$$
6		mndassd.6	$$⊢\phi \to Z\in B$$
7	1 2	mndass	$$⊢\left(G\in \mathrm{Mnd}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)$$
8	3 4 5 6 7	syl13anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)$$