Metamath Proof Explorer


Theorem lpirring

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

Ref Expression
Assertion lpirring R LPIR R Ring

Proof

Step Hyp Ref Expression
1 eqid LPIdeal R = LPIdeal R
2 eqid LIdeal R = LIdeal R
3 1 2 islpir R LPIR R Ring LIdeal R = LPIdeal R
4 3 simplbi R LPIR R Ring