Theorem grpsgrp

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

	Ref	Expression
Assertion	grpsgrp	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Smgrp )

Proof

Step	Hyp	Ref	Expression
1		grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
2		mndsgrp	⊢ ( 𝐺 ∈ Mnd → 𝐺 ∈ Smgrp )
3	1 2	syl	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Smgrp )