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

Theorem ablcmn 18399
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 18397 . 2 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
21simprbi 483 1 (𝐺 ∈ Abel → 𝐺 ∈ CMnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  Grpcgrp 17623  CMndccmn 18393  Abelcabl 18394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722  df-abl 18396
This theorem is referenced by:  ablcom  18410  abl32  18414  ablsub4  18418  mulgdi  18432  ghmabl  18438  ghmplusg  18449  ablcntzd  18460  prdsabld  18465  gsumsubgcl  18520  gsummulgz  18543  gsuminv  18546  gsumsub  18548  telgsumfzslem  18585  telgsums  18590  ringcmn  18781  lmodcmn  19113  clmsub4  23106  lgseisenlem4  25302
  Copyright terms: Public domain W3C validator