Theorem ablcmn 19717

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

Syntax hints:   → wi 4   ∈ wcel 2109  Grpcgrp 18865  CMndccmn 19710  Abelcabl 19711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921  df-abl 19713

This theorem is referenced by:  ablcmnd  19718  ablcom  19729  abl32  19733  ablsub4  19740  mulgdi  19756  ghmabl  19762  ghmplusg  19776  ablcntzd  19787  prdsabld  19792  gsumsubgcl  19850  gsummulgz  19873  gsuminv  19876  gsumsub  19878  telgsumfzslem  19918  telgsums  19923  ringcmn  20191  lmodcmn  20816  clmsub4  25006  lgseisenlem4  27289  primrootspoweq0  42094  aks6d1c6lem4  42161