Theorem ablcmn 19728

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

Syntax hints:   → wi 4   ∈ wcel 2114  Grpcgrp 18875  CMndccmn 19721  Abelcabl 19722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910  df-abl 19724

This theorem is referenced by:  ablcmnd  19729  ablcom  19740  abl32  19744  ablsub4  19751  mulgdi  19767  ghmabl  19773  ghmplusg  19787  ablcntzd  19798  prdsabld  19803  gsumsubgcl  19861  gsummulgz  19884  gsuminv  19887  gsumsub  19889  telgsumfzslem  19929  telgsums  19934  ringcmn  20229  lmodcmn  20873  clmsub4  25074  lgseisenlem4  27357  primrootspoweq0  42476  aks6d1c6lem4  42543