Theorem ablcmn 19852

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 19849	. 2 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
2	1	simprbi 502	1 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ CMnd)

Syntax hints:   → wi 4   ∈ wcel 2143  Grpcgrp 18995  CMndccmn 19845  Abelcabl 19846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-abl 19848

This theorem is referenced by:  ablcmnd  19853  ablcom  19864  abl32  19868  ablsub4  19875  mulgdi  19891  ghmabl  19897  ghmplusg  19911  ablcntzd  19922  prdsabld  19927  gsumsubgcl  19985  gsummulgz  20008  gsuminv  20011  gsumsub  20013  telgsumfzslem  20053  telgsums  20058  ringcmn  20361  lmodcmn  21031  clmsub4  25265  lgseisenlem4  27542  primrootspoweq0  42873  aks6d1c6lem4  42940