Theorem ablcmn 19714

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

Syntax hints:   → wi 4   ∈ wcel 2113  Grpcgrp 18861  CMndccmn 19707  Abelcabl 19708

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906  df-abl 19710

This theorem is referenced by:  ablcmnd  19715  ablcom  19726  abl32  19730  ablsub4  19737  mulgdi  19753  ghmabl  19759  ghmplusg  19773  ablcntzd  19784  prdsabld  19789  gsumsubgcl  19847  gsummulgz  19870  gsuminv  19873  gsumsub  19875  telgsumfzslem  19915  telgsums  19920  ringcmn  20215  lmodcmn  20859  clmsub4  25060  lgseisenlem4  27343  primrootspoweq0  42299  aks6d1c6lem4  42366