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

Theorem ablcmn 15095
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 15093 . 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 1684   Grpcgrp 14362  CMndccmn 15089   Abelcabel 15090
This theorem is referenced by:  ablcom  15106  abl32  15110  ablsub4  15114  mulgdi  15126  ghmplusg  15138  ablcntzd  15149  prdsabld  15154  gsumsubgcl  15202  gsummulgz  15215  gsuminv  15218  gsumsub  15219  rngcmn  15371  lmodcmn  15673  lgseisenlem4  20591
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-abl 15092
  Copyright terms: Public domain W3C validator