Theorem ablcmn 18905

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

Syntax hints:   → wi 4   ∈ wcel 2111  Grpcgrp 18095  CMndccmn 18898  Abelcabl 18899

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-abl 18901

This theorem is referenced by:  ablcom  18916  abl32  18920  ablsub4  18926  mulgdi  18940  ghmabl  18946  ghmplusg  18959  ablcntzd  18970  prdsabld  18975  gsumsubgcl  19033  gsummulgz  19056  gsuminv  19059  gsumsub  19061  telgsumfzslem  19101  telgsums  19106  ringcmn  19327  lmodcmn  19675  clmsub4  23711  lgseisenlem4  25962  ablcmnd  39442