Metamath Proof Explorer

Theorem cmnmnd

Description: A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015)

Ref Expression
Assertion cmnmnd 
|- ( G e. CMnd -> G e. Mnd )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` G ) = ( Base ` G )
2 eqid 
 |-  ( +g ` G ) = ( +g ` G )
3 1 2 iscmn 
 |-  ( G e. CMnd <-> ( G e. Mnd /\ A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) )
4 3 simplbi 
 |-  ( G e. CMnd -> G e. Mnd )