Metamath Proof Explorer

Theorem zringgrp

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

Ref Expression
Assertion zringgrp 
|- ZZring e. Grp

Proof

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