Theorem ablcmn 19856

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

Syntax hints:   → wi 4   ∈ wcel 2149  Grpcgrp 18999  CMndccmn 19849  Abelcabl 19850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-abl 19852

This theorem is referenced by:  ablcmnd  19857  ablcom  19868  abl32  19872  ablsub4  19879  mulgdi  19895  ghmabl  19901  ghmplusg  19915  ablcntzd  19926  prdsabld  19931  gsumsubgcl  19989  gsummulgz  20012  gsuminv  20015  gsumsub  20017  telgsumfzslem  20057  telgsums  20062  ringcmn  20364  lmodcmn  21008  clmsub4  25233  lgseisenlem4  27507  primrootspoweq0  42762  aks6d1c6lem4  42829