Theorem ablcmnd

Description: An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024)

	Ref	Expression
Hypothesis	ablcmnd.1	$$⊢\phi \to G\in \mathrm{Abel}$$
Assertion	ablcmnd	$$⊢\phi \to G\in \mathrm{CMnd}$$

Proof

Step	Hyp	Ref	Expression
1		ablcmnd.1	$$⊢\phi \to G\in \mathrm{Abel}$$
2		ablcmn	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{CMnd}$$
3	1 2	syl	$$⊢\phi \to G\in \mathrm{CMnd}$$