Theorem ablcmn 19805

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

Syntax hints:   → wi 4   ∈ wcel 2108  Grpcgrp 18951  CMndccmn 19798  Abelcabl 19799

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-abl 19801

This theorem is referenced by:  ablcmnd  19806  ablcom  19817  abl32  19821  ablsub4  19828  mulgdi  19844  ghmabl  19850  ghmplusg  19864  ablcntzd  19875  prdsabld  19880  gsumsubgcl  19938  gsummulgz  19961  gsuminv  19964  gsumsub  19966  telgsumfzslem  20006  telgsums  20011  ringcmn  20279  lmodcmn  20908  clmsub4  25139  lgseisenlem4  27422  primrootspoweq0  42107  aks6d1c6lem4  42174