Theorem ablcmn 19699

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

Syntax hints:   → wi 4   ∈ wcel 2111  Grpcgrp 18846  CMndccmn 19692  Abelcabl 19693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904  df-abl 19695

This theorem is referenced by:  ablcmnd  19700  ablcom  19711  abl32  19715  ablsub4  19722  mulgdi  19738  ghmabl  19744  ghmplusg  19758  ablcntzd  19769  prdsabld  19774  gsumsubgcl  19832  gsummulgz  19855  gsuminv  19858  gsumsub  19860  telgsumfzslem  19900  telgsums  19905  ringcmn  20200  lmodcmn  20843  clmsub4  25033  lgseisenlem4  27316  primrootspoweq0  42147  aks6d1c6lem4  42214