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 CMnd

Proof of Theorem ablcmn
StepHypRef Expression
1 isabl 15109 . 2 CMnd
21simprbi 450 1 CMnd
 Colors of variables: wff set class Syntax hints:   wi 4   wcel 1696  cgrp 14378  CMndccmn 15105  cabel 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