Description: Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isabld.b | ||
isabld.p | |||
isabld.g | |||
isabld.c | |||
Assertion | isabld |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isabld.b | ||
2 | isabld.p | ||
3 | isabld.g | ||
4 | isabld.c | ||
5 | grpmnd | ||
6 | 3 5 | syl | |
7 | 1 2 6 4 | iscmnd | |
8 | isabl | ||
9 | 3 7 8 | sylanbrc |