Theorem lringring

Description: A local ring is a ring. (Contributed by Jim Kingdon, 20-Feb-2025) (Revised by SN, 23-Feb-2025)

	Ref	Expression
Assertion	lringring	⊢ ( 𝑅 ∈ LRing → 𝑅 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		lringnzr	⊢ ( 𝑅 ∈ LRing → 𝑅 ∈ NzRing )
2		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
3	1 2	syl	⊢ ( 𝑅 ∈ LRing → 𝑅 ∈ Ring )