This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem crngorngo

Description: A commutative ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Assertion crngorngo ⊢ R ∈ CRingOps → R ∈ RingOps

Proof

Step Hyp Ref Expression
1 iscrngo ⊢ R ∈ CRingOps ↔ R ∈ RingOps ∧ R ∈ Com2
2 1 simplbi ⊢ R ∈ CRingOps → R ∈ RingOps