Theorem ablcmn 19829

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

Syntax hints:   → wi 4   ∈ wcel 2108  Grpcgrp 18973  CMndccmn 19822  Abelcabl 19823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-abl 19825

This theorem is referenced by:  ablcmnd  19830  ablcom  19841  abl32  19845  ablsub4  19852  mulgdi  19868  ghmabl  19874  ghmplusg  19888  ablcntzd  19899  prdsabld  19904  gsumsubgcl  19962  gsummulgz  19985  gsuminv  19988  gsumsub  19990  telgsumfzslem  20030  telgsums  20035  ringcmn  20305  lmodcmn  20930  clmsub4  25158  lgseisenlem4  27440  primrootspoweq0  42063  aks6d1c6lem4  42130