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

Theorem ablcmn 17371
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 17369 . 2  |-  ( G  e.  Abel  <->  ( G  e. 
Grp  /\  G  e. CMnd ) )
21simprbi 465 1  |-  ( G  e.  Abel  ->  G  e. CMnd
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   Grpcgrp 16620  CMndccmn 17365   Abelcabl 17366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449  df-abl 17368
This theorem is referenced by:  ablcom  17382  abl32  17386  ablsub4  17390  mulgdi  17402  ghmabl  17408  ghmplusg  17419  ablcntzd  17430  prdsabld  17435  gsumsubgcl  17488  gsummulgz  17511  gsuminv  17514  gsumsub  17516  telgsumfzslem  17553  telgsums  17558  ringcmn  17746  lmodcmn  18071  lgseisenlem4  24143
  Copyright terms: Public domain W3C validator