Metamath Proof Explorer

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 \in NzRing \to R \in Ring$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ 1_{R} = 1_{R}$
2		eqid	$⊢ 0_{R} = 0_{R}$
3	1 2	isnzr	$⊢ R \in NzRing \leftrightarrow (R \in Ring \land 1_{R} \neq 0_{R})$
4	3	simplbi	$⊢ R \in NzRing \to R \in Ring$