Theorem ablcmn 19762

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

Syntax hints:   → wi 4   ∈ wcel 2114  Grpcgrp 18909  CMndccmn 19755  Abelcabl 19756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-abl 19758

This theorem is referenced by:  ablcmnd  19763  ablcom  19774  abl32  19778  ablsub4  19785  mulgdi  19801  ghmabl  19807  ghmplusg  19821  ablcntzd  19832  prdsabld  19837  gsumsubgcl  19895  gsummulgz  19918  gsuminv  19921  gsumsub  19923  telgsumfzslem  19963  telgsums  19968  ringcmn  20263  lmodcmn  20905  clmsub4  25073  lgseisenlem4  27341  primrootspoweq0  42545  aks6d1c6lem4  42612