Theorem ablcmn 19404

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

Syntax hints:   → wi 4   ∈ wcel 2110  Grpcgrp 18588  CMndccmn 19397  Abelcabl 19398

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-abl 19400

This theorem is referenced by:  ablcom  19415  abl32  19419  ablsub4  19425  mulgdi  19439  ghmabl  19445  ghmplusg  19458  ablcntzd  19469  prdsabld  19474  gsumsubgcl  19532  gsummulgz  19555  gsuminv  19558  gsumsub  19560  telgsumfzslem  19600  telgsums  19605  ringcmn  19831  lmodcmn  20182  clmsub4  24280  lgseisenlem4  26537  ablcmnd  40248