Theorem grpsgrp

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

	Ref	Expression
Assertion	grpsgrp	|- ( G e. Grp -> G e. Smgrp )

Proof

Step	Hyp	Ref	Expression
1		grpmnd	|- ( G e. Grp -> G e. Mnd )
2		mndsgrp	|- ( G e. Mnd -> G e. Smgrp )
3	1 2	syl	|- ( G e. Grp -> G e. Smgrp )