Description: Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isabli.g | |
|
isabli.b | |
||
isabli.p | |
||
isabli.c | |
||
Assertion | isabli | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isabli.g | |
|
2 | isabli.b | |
|
3 | isabli.p | |
|
4 | isabli.c | |
|
5 | 4 | rgen2 | |
6 | 2 3 | isabl2 | |
7 | 1 5 6 | mpbir2an | |