Theorem ablcmn 19308

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

Syntax hints:   → wi 4   ∈ wcel 2108  Grpcgrp 18492  CMndccmn 19301  Abelcabl 19302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-abl 19304

This theorem is referenced by:  ablcom  19319  abl32  19323  ablsub4  19329  mulgdi  19343  ghmabl  19349  ghmplusg  19362  ablcntzd  19373  prdsabld  19378  gsumsubgcl  19436  gsummulgz  19459  gsuminv  19462  gsumsub  19464  telgsumfzslem  19504  telgsums  19509  ringcmn  19735  lmodcmn  20086  clmsub4  24175  lgseisenlem4  26431  ablcmnd  40165