Theorem ablcmn 19754

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

Syntax hints:   → wi 4   ∈ wcel 2098  Grpcgrp 18898  CMndccmn 19747  Abelcabl 19748

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-in 3951  df-abl 19750

This theorem is referenced by:  ablcmnd  19755  ablcom  19766  abl32  19770  ablsub4  19777  mulgdi  19793  ghmabl  19799  ghmplusg  19813  ablcntzd  19824  prdsabld  19829  gsumsubgcl  19887  gsummulgz  19910  gsuminv  19913  gsumsub  19915  telgsumfzslem  19955  telgsums  19960  ringcmn  20230  lmodcmn  20805  clmsub4  25077  lgseisenlem4  27356  primrootspoweq0  41709  aks6d1c6lem4  41776