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 499	1 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ CMnd)

Syntax hints:   → wi 4   ∈ wcel 2107  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 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495  df-in 3941  df-abl 18901

This theorem is referenced by:  ablcom  18916  abl32  18920  ablsub4  18925  mulgdi  18939  ghmabl  18945  ghmplusg  18958  ablcntzd  18969  prdsabld  18974  gsumsubgcl  19032  gsummulgz  19055  gsuminv  19058  gsumsub  19060  telgsumfzslem  19100  telgsums  19105  ringcmn  19323  lmodcmn  19674  clmsub4  23702  lgseisenlem4  25946