Theorem ablcmn 19994

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Grpcgrp 19137  CMndccmn 19987  Abelcabl 19988

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-abl 19990

This theorem is used by:  ablcmnd  19995  ablcom  20006  abl32  20010  ablsub4  20017  mulgdi  20033  ghmabl  20039  ghmplusg  20053  ablcntzd  20064  prdsabld  20069  gsumsubgcl  20127  gsummulgz  20150  gsuminv  20153  gsumsub  20155  telgsumfzslem  20195  telgsums  20200  ringcmn  20504  lmodcmn  21178  clmsub4  25420  lgseisenlem4  27698  primrootspoweq0  43136  aks6d1c6lem4  43203