Theorem ablcmn 19693

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

Syntax hints:   → wi 4   ∈ wcel 2109  Grpcgrp 18841  CMndccmn 19686  Abelcabl 19687

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918  df-abl 19689

This theorem is referenced by:  ablcmnd  19694  ablcom  19705  abl32  19709  ablsub4  19716  mulgdi  19732  ghmabl  19738  ghmplusg  19752  ablcntzd  19763  prdsabld  19768  gsumsubgcl  19826  gsummulgz  19849  gsuminv  19852  gsumsub  19854  telgsumfzslem  19894  telgsums  19899  ringcmn  20167  lmodcmn  20792  clmsub4  24982  lgseisenlem4  27265  primrootspoweq0  42067  aks6d1c6lem4  42134