Metamath Proof Explorer


Theorem grpass

Description: A group operation is associative. (Contributed by NM, 14-Aug-2011)

Ref Expression
Hypotheses grpcl.b B = Base G
grpcl.p + ˙ = + G
Assertion grpass G Grp X B Y B Z B X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z

Proof

Step Hyp Ref Expression
1 grpcl.b B = Base G
2 grpcl.p + ˙ = + G
3 grpmnd G Grp G Mnd
4 1 2 mndass G Mnd X B Y B Z B X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z
5 3 4 sylan G Grp X B Y B Z B X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z