Theorem ablcmn 19753

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

Syntax hints:   → wi 4   ∈ wcel 2119  Grpcgrp 18900  CMndccmn 19746  Abelcabl 19747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890  df-abl 19749

This theorem is referenced by:  ablcmnd  19754  ablcom  19765  abl32  19769  ablsub4  19776  mulgdi  19792  ghmabl  19798  ghmplusg  19812  ablcntzd  19823  prdsabld  19828  gsumsubgcl  19886  gsummulgz  19909  gsuminv  19912  gsumsub  19914  telgsumfzslem  19954  telgsums  19959  ringcmn  20254  lmodcmn  20900  clmsub4  25091  lgseisenlem4  27359  primrootspoweq0  42591  aks6d1c6lem4  42658