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	Could not format assertion : No typesetting found for |- ( R e. PrmRing -> R e. Ring ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		prmringnzring	Could not format ( R e. PrmRing -> R e. NzRing ) : No typesetting found for |- ( R e. PrmRing -> R e. NzRing ) with typecode |-
2		nzrring	$$⊢R\in \mathrm{NzRing}\to R\in \mathrm{Ring}$$
3	1 2	syl	Could not format ( R e. PrmRing -> R e. Ring ) : No typesetting found for |- ( R e. PrmRing -> R e. Ring ) with typecode |-