Theorem grpsgrp

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

	Ref	Expression
Assertion	grpsgrp	Could not format assertion : No typesetting found for |- ( G e. Grp -> G e. Smgrp ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		grpmnd	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Mnd}$$
2		mndsgrp	Could not format ( G e. Mnd -> G e. Smgrp ) : No typesetting found for |- ( G e. Mnd -> G e. Smgrp ) with typecode |-
3	1 2	syl	Could not format ( G e. Grp -> G e. Smgrp ) : No typesetting found for |- ( G e. Grp -> G e. Smgrp ) with typecode |-