Theorem ablcmn 19901

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Grpcgrp 19044  CMndccmn 19894  Abelcabl 19895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-abl 19897

This theorem is used by:  ablcmnd  19902  ablcom  19913  abl32  19917  ablsub4  19924  mulgdi  19940  ghmabl  19946  ghmplusg  19960  ablcntzd  19971  prdsabld  19976  gsumsubgcl  20034  gsummulgz  20057  gsuminv  20060  gsumsub  20062  telgsumfzslem  20102  telgsums  20107  ringcmn  20410  lmodcmn  21081  clmsub4  25316  lgseisenlem4  27593  primrootspoweq0  42931  aks6d1c6lem4  42998