Theorem ablcmn 19393

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

Syntax hints:   → wi 4   ∈ wcel 2106  Grpcgrp 18577  CMndccmn 19386  Abelcabl 19387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-abl 19389

This theorem is referenced by:  ablcom  19404  abl32  19408  ablsub4  19414  mulgdi  19428  ghmabl  19434  ghmplusg  19447  ablcntzd  19458  prdsabld  19463  gsumsubgcl  19521  gsummulgz  19544  gsuminv  19547  gsumsub  19549  telgsumfzslem  19589  telgsums  19594  ringcmn  19820  lmodcmn  20171  clmsub4  24269  lgseisenlem4  26526  ablcmnd  40239