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 ringRing

Proof

Step Hyp Ref Expression
1 zringcrng ringCRing
2 crngring ringCRingringRing
3 1 2 ax-mp ringRing