Metamath Proof Explorer


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
Assertion mndass G Mnd X B Y B Z B X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z

Proof

Step Hyp Ref Expression
1 mndcl.b B = Base G
2 mndcl.p + ˙ = + G
3 mndsgrp G Mnd G Smgrp
4 1 2 sgrpass G Smgrp X B Y B Z B X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z
5 3 4 sylan G Mnd X B Y B Z B X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z