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

Proof

Step Hyp Ref Expression
1 zringcrng ring ∈ CRing
2 crngring ( ℤring ∈ CRing → ℤring ∈ Ring )
3 1 2 ax-mp ring ∈ Ring