Metamath Proof Explorer

Theorem crngorngo

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

Ref Expression
Assertion crngorngo 
|- ( R e. CRingOps -> R e. RingOps )

Proof

Step Hyp Ref Expression
1 iscrngo 
 |-  ( R e. CRingOps <-> ( R e. RingOps /\ R e. Com2 ) )
2 1 simplbi 
 |-  ( R e. CRingOps -> R e. RingOps )