Metamath Proof Explorer

Theorem lnrring

Description: Left-Noetherian rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Assertion lnrring 
|- ( A e. LNoeR -> A e. Ring )

Proof

Step Hyp Ref Expression
1 islnr 
 |-  ( A e. LNoeR <-> ( A e. Ring /\ ( ringLMod ` A ) e. LNoeM ) )
2 1 simplbi 
 |-  ( A e. LNoeR -> A e. Ring )