Metamath Proof Explorer

Theorem zringring

Description: The ring of integers is a ring. (Contributed by AV, 20-May-2019) (Revised by AV, 9-Jun-2019) (Proof shortened by AV, 13-Jun-2019)

Ref Expression
Assertion zringring 
|- ZZring e. Ring

Proof

Step Hyp Ref Expression
1 zringcrng 
 |-  ZZring e. CRing
2 crngring 
 |-  ( ZZring e. CRing -> ZZring e. Ring )
3 1 2 ax-mp 
 |-  ZZring e. Ring