Metamath Proof Explorer

Theorem prmrngring

Description: A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 18-Jun-2026) (Proof shortened by AV, 26-Jun-2026)

Ref Expression
Assertion prmrngring 
|- ( R e. PrmRing -> R e. Ring )

Proof

Step Hyp Ref Expression
1 prmringnzring 
 |-  ( R e. PrmRing -> R e. NzRing )
2 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
3 1 2 syl 
 |-  ( R e. PrmRing -> R e. Ring )