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

Theorem ablcmn 18892
 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 18889 . 2 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
21simprbi 499 1 (𝐺 ∈ Abel → 𝐺 ∈ CMnd)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2114  Grpcgrp 18082  CMndccmn 18885  Abelcabl 18886 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2792 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-v 3475  df-in 3920  df-abl 18888 This theorem is referenced by:  ablcom  18903  abl32  18907  ablsub4  18912  mulgdi  18926  ghmabl  18932  ghmplusg  18945  ablcntzd  18956  prdsabld  18961  gsumsubgcl  19019  gsummulgz  19042  gsuminv  19045  gsumsub  19047  telgsumfzslem  19087  telgsums  19092  ringcmn  19310  lmodcmn  19658  clmsub4  23690  lgseisenlem4  25941
 Copyright terms: Public domain W3C validator