Metamath Proof Explorer


Theorem isabld

Description: Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013)

Ref Expression
Hypotheses isabld.b φ B = Base G
isabld.p φ + ˙ = + G
isabld.g φ G Grp
isabld.c φ x B y B x + ˙ y = y + ˙ x
Assertion isabld φ G Abel

Proof

Step Hyp Ref Expression
1 isabld.b φ B = Base G
2 isabld.p φ + ˙ = + G
3 isabld.g φ G Grp
4 isabld.c φ x B y B x + ˙ y = y + ˙ x
5 3 grpmndd φ G Mnd
6 1 2 5 4 iscmnd φ G CMnd
7 isabl G Abel G Grp G CMnd
8 3 6 7 sylanbrc φ G Abel