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	|- ( R e. NzRing -> R e. Ring )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( 1r ` R ) = ( 1r ` R )
2		eqid	|- ( 0g ` R ) = ( 0g ` R )
3	1 2	isnzr	|- ( R e. NzRing <-> ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) )
4	3	simplbi	|- ( R e. NzRing -> R e. Ring )