Theorem ablcmn 19914

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Grpcgrp 19057  CMndccmn 19907  Abelcabl 19908

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906  df-abl 19910

This theorem is used by:  ablcmnd  19915  ablcom  19926  abl32  19930  ablsub4  19937  mulgdi  19953  ghmabl  19959  ghmplusg  19973  ablcntzd  19984  prdsabld  19989  gsumsubgcl  20047  gsummulgz  20070  gsuminv  20073  gsumsub  20075  telgsumfzslem  20115  telgsums  20120  ringcmn  20423  lmodcmn  21094  clmsub4  25334  lgseisenlem4  27614  primrootspoweq0  42972  aks6d1c6lem4  43039