Metamath Proof Explorer

Theorem zringabl

Description: The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019)

Ref Expression
Assertion zringabl 
|- ZZring e. Abel

Proof

Step Hyp Ref Expression
1 zringring 
 |-  ZZring e. Ring
2 ringabl 
 |-  ( ZZring e. Ring -> ZZring e. Abel )
3 1 2 ax-mp 
 |-  ZZring e. Abel