Theorem nzrring

Description: A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Assertion	nzrring	⊢ ( 𝑅 ∈ 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 )