Theorem ablcmn 18199

Description: An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)

Assertion

Ref	Expression
ablcmn	|- ( G e. Abel -> G e. CMnd )

Proof of Theorem ablcmn

Step	Hyp	Ref	Expression
1		isabl 18197	. 2 |- ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
2	1	simprbi 480	1 |- ( G e. Abel -> G e. CMnd )

Syntax hints:   -> wi 4   e. wcel 1990   Grpcgrp 17422  CMndccmn 18193   Abelcabl 18194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-abl 18196

This theorem is referenced by:  ablcom  18210  abl32  18214  ablsub4  18218  mulgdi  18232  ghmabl  18238  ghmplusg  18249  ablcntzd  18260  prdsabld  18265  gsumsubgcl  18320  gsummulgz  18343  gsuminv  18346  gsumsub  18348  telgsumfzslem  18385  telgsums  18390  ringcmn  18581  lmodcmn  18911  clmsub4  22906  lgseisenlem4  25103