Metamath Proof Explorer

Theorem nzrring

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

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