Metamath Proof Explorer


Theorem grpass

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

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

Proof

Step Hyp Ref Expression
1 grpcl.b B=BaseG
2 grpcl.p +˙=+G
3 grpmnd GGrpGMnd
4 1 2 mndass GMndXBYBZBX+˙Y+˙Z=X+˙Y+˙Z
5 3 4 sylan GGrpXBYBZBX+˙Y+˙Z=X+˙Y+˙Z