Theorem nzrringOLD

Description: Obsolete version of nzrring as of 23-Feb-2025. (Contributed by Stefan O'Rear, 24-Feb-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	nzrringOLD	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
2		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
3	1 2	isnzr	⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
4	3	simplbi	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )