Theorem ablcmn 19756

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

Syntax hints:   → wi 4   ∈ wcel 2114  Grpcgrp 18903  CMndccmn 19749  Abelcabl 19750

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 3432  df-in 3897  df-abl 19752

This theorem is referenced by:  ablcmnd  19757  ablcom  19768  abl32  19772  ablsub4  19779  mulgdi  19795  ghmabl  19801  ghmplusg  19815  ablcntzd  19826  prdsabld  19831  gsumsubgcl  19889  gsummulgz  19912  gsuminv  19915  gsumsub  19917  telgsumfzslem  19957  telgsums  19962  ringcmn  20257  lmodcmn  20899  clmsub4  25086  lgseisenlem4  27358  primrootspoweq0  42562  aks6d1c6lem4  42629