Theorem ablcmn 19768

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

Syntax hints:   → wi 4   ∈ wcel 2108  Grpcgrp 18916  CMndccmn 19761  Abelcabl 19762

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933  df-abl 19764

This theorem is referenced by:  ablcmnd  19769  ablcom  19780  abl32  19784  ablsub4  19791  mulgdi  19807  ghmabl  19813  ghmplusg  19827  ablcntzd  19838  prdsabld  19843  gsumsubgcl  19901  gsummulgz  19924  gsuminv  19927  gsumsub  19929  telgsumfzslem  19969  telgsums  19974  ringcmn  20242  lmodcmn  20867  clmsub4  25057  lgseisenlem4  27341  primrootspoweq0  42119  aks6d1c6lem4  42186