Theorem grpsgrp

Description: A group is a semigroup. (Contributed by AV, 28-Aug-2021)

	Ref	Expression
Assertion	grpsgrp	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Smgrp}$$

Proof

Step	Hyp	Ref	Expression
1		grpmnd	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Mnd}$$
2		mndsgrp	$$⊢G\in \mathrm{Mnd}\to G\in \mathrm{Smgrp}$$
3	1 2	syl	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Smgrp}$$