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

Theorem ablcmn 18551
 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 18549 . 2 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
21simprbi 492 1 (𝐺 ∈ Abel → 𝐺 ∈ CMnd)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2166  Grpcgrp 17775  CMndccmn 18545  Abelcabl 18546 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2802 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-v 3415  df-in 3804  df-abl 18548 This theorem is referenced by:  ablcom  18562  abl32  18566  ablsub4  18570  mulgdi  18584  ghmabl  18590  ghmplusg  18601  ablcntzd  18612  prdsabld  18617  gsumsubgcl  18672  gsummulgz  18695  gsuminv  18698  gsumsub  18700  telgsumfzslem  18738  telgsums  18743  ringcmn  18934  lmodcmn  19266  clmsub4  23274  lgseisenlem4  25515
 Copyright terms: Public domain W3C validator