Theorem ablcmn 19741

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

Syntax hints:   → wi 4   ∈ wcel 2099  Grpcgrp 18889  CMndccmn 19734  Abelcabl 19735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954  df-abl 19737

This theorem is referenced by:  ablcmnd  19742  ablcom  19753  abl32  19757  ablsub4  19764  mulgdi  19780  ghmabl  19786  ghmplusg  19800  ablcntzd  19811  prdsabld  19816  gsumsubgcl  19874  gsummulgz  19897  gsuminv  19900  gsumsub  19902  telgsumfzslem  19942  telgsums  19947  ringcmn  20217  lmodcmn  20792  clmsub4  25032  lgseisenlem4  27310  primrootspoweq0  41577  aks6d1c6lem4  41645

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »