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 ring Ring


Step Hyp Ref Expression
1 zringcrng ring CRing
2 crngring ring CRing ring Ring
3 1 2 ax-mp ring Ring