Theorem ablcmn 20010

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Grpcgrp 19153  CMndccmn 20003  Abelcabl 20004

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4090  df-abl 20006

This theorem is used by:  ablcmnd  20011  ablcom  20022  abl32  20026  ablsub4  20033  mulgdi  20049  ghmabl  20055  ghmplusg  20069  ablcntzd  20080  prdsabld  20085  gsumsubgcl  20143  gsummulgz  20166  gsuminv  20169  gsumsub  20171  telgsumfzslem  20211  telgsums  20216  ringcmn  20520  lmodcmn  21194  clmsub4  25436  lgseisenlem4  27714  primrootspoweq0  43265  aks6d1c6lem4  43332