Theorem sgrpmgm

Description: A semigroup is a magma. (Contributed by FL, 2-Nov-2009) (Revised by AV, 6-Jan-2020)

	Ref	Expression
Assertion	sgrpmgm	$$⊢M\in \mathrm{Smgrp}\to M\in \mathrm{Mgm}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
2		eqid	$$⊢{+}_M={+}_M$$
3	1 2	issgrp	$$⊢M\in \mathrm{Smgrp}\leftrightarrow \left(M\in \mathrm{Mgm}\wedge \forall x\in {\mathrm{Base}}_M\forall y\in {\mathrm{Base}}_M\forall z\in {\mathrm{Base}}_M\left(x{+}_{M}y\right){+}_{M}z=x{+}_M\left(y{+}_{M}z\right)\right)$$
4	3	simplbi	$$⊢M\in \mathrm{Smgrp}\to M\in \mathrm{Mgm}$$