Theorem ablcmn 19716

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

Syntax hints:   → wi 4   ∈ wcel 2113  Grpcgrp 18863  CMndccmn 19709  Abelcabl 19710

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-abl 19712

This theorem is referenced by:  ablcmnd  19717  ablcom  19728  abl32  19732  ablsub4  19739  mulgdi  19755  ghmabl  19761  ghmplusg  19775  ablcntzd  19786  prdsabld  19791  gsumsubgcl  19849  gsummulgz  19872  gsuminv  19875  gsumsub  19877  telgsumfzslem  19917  telgsums  19922  ringcmn  20217  lmodcmn  20861  clmsub4  25062  lgseisenlem4  27345  primrootspoweq0  42360  aks6d1c6lem4  42427