Theorem ablcmn 19819

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

Syntax hints:   → wi 4   ∈ wcel 2105  Grpcgrp 18963  CMndccmn 19812  Abelcabl 19813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969  df-abl 19815

This theorem is referenced by:  ablcmnd  19820  ablcom  19831  abl32  19835  ablsub4  19842  mulgdi  19858  ghmabl  19864  ghmplusg  19878  ablcntzd  19889  prdsabld  19894  gsumsubgcl  19952  gsummulgz  19975  gsuminv  19978  gsumsub  19980  telgsumfzslem  20020  telgsums  20025  ringcmn  20295  lmodcmn  20924  clmsub4  25152  lgseisenlem4  27436  primrootspoweq0  42087  aks6d1c6lem4  42154