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

Theorem ablcmn 19805
Description: An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
Assertion
Ref Expression
ablcmn (𝐺 ∈ Abel → 𝐺 ∈ CMnd)

Proof of Theorem ablcmn
StepHypRef Expression
1 isabl 19802 . 2 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
21simprbi 496 1 (𝐺 ∈ Abel → 𝐺 ∈ CMnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  Grpcgrp 18951  CMndccmn 19798  Abelcabl 19799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-abl 19801
This theorem is referenced by:  ablcmnd  19806  ablcom  19817  abl32  19821  ablsub4  19828  mulgdi  19844  ghmabl  19850  ghmplusg  19864  ablcntzd  19875  prdsabld  19880  gsumsubgcl  19938  gsummulgz  19961  gsuminv  19964  gsumsub  19966  telgsumfzslem  20006  telgsums  20011  ringcmn  20279  lmodcmn  20908  clmsub4  25139  lgseisenlem4  27422  primrootspoweq0  42107  aks6d1c6lem4  42174
  Copyright terms: Public domain W3C validator