Metamath Proof Explorer


Theorem ablcom

Description: An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011)

Ref Expression
Hypotheses ablcom.b B=BaseG
ablcom.p +˙=+G
Assertion ablcom GAbelXBYBX+˙Y=Y+˙X

Proof

Step Hyp Ref Expression
1 ablcom.b B=BaseG
2 ablcom.p +˙=+G
3 ablcmn GAbelGCMnd
4 1 2 cmncom GCMndXBYBX+˙Y=Y+˙X
5 3 4 syl3an1 GAbelXBYBX+˙Y=Y+˙X