Theorem ablcmn 19827

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

Step	Hyp	Ref	Expression
1		isabl 19824	. 2 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
2	1	simprbi 501	1 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ CMnd)

Syntax hints:   → wi 4   ∈ wcel 2142  Grpcgrp 18975  CMndccmn 19820  Abelcabl 19821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911  df-abl 19823

This theorem is referenced by:  ablcmnd  19828  ablcom  19839  abl32  19843  ablsub4  19850  mulgdi  19866  ghmabl  19872  ghmplusg  19886  ablcntzd  19897  prdsabld  19902  gsumsubgcl  19960  gsummulgz  19983  gsuminv  19986  gsumsub  19988  telgsumfzslem  20028  telgsums  20033  ringcmn  20328  lmodcmn  20974  clmsub4  25165  lgseisenlem4  27439  primrootspoweq0  42720  aks6d1c6lem4  42787