Theorem sgrpmgm

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

	Ref	Expression
Assertion	sgrpmgm	Could not format assertion : No typesetting found for |- ( M e. Smgrp -> M e. Mgm ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
2		eqid	$$⊢{+}_M={+}_M$$
3	1 2	issgrp	Could not format ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. ( Base ` M ) A. y e. ( Base ` M ) A. z e. ( Base ` M ) ( ( x ( +g ` M ) y ) ( +g ` M ) z ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) ) ) : No typesetting found for |- ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. ( Base ` M ) A. y e. ( Base ` M ) A. z e. ( Base ` M ) ( ( x ( +g ` M ) y ) ( +g ` M ) z ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) ) ) with typecode |-
4	3	simplbi	Could not format ( M e. Smgrp -> M e. Mgm ) : No typesetting found for |- ( M e. Smgrp -> M e. Mgm ) with typecode |-