MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ablcmn Unicode version

Theorem ablcmn 15111
Description: An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
Assertion
Ref Expression
ablcmn  |-  ( G  e.  Abel  ->  G  e. CMnd
)

Proof of Theorem ablcmn
StepHypRef Expression
1 isabl 15109 . 2  |-  ( G  e.  Abel  <->  ( G  e. 
Grp  /\  G  e. CMnd ) )
21simprbi 450 1  |-  ( G  e.  Abel  ->  G  e. CMnd
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   Grpcgrp 14378  CMndccmn 15105   Abelcabel 15106
This theorem is referenced by:  ablcom  15122  abl32  15126  ablsub4  15130  mulgdi  15142  ghmplusg  15154  ablcntzd  15165  prdsabld  15170  gsumsubgcl  15218  gsummulgz  15231  gsuminv  15234  gsumsub  15235  rngcmn  15387  lmodcmn  15689  lgseisenlem4  20607
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-abl 15108
  Copyright terms: Public domain W3C validator