Theorem mndmgm

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

	Ref	Expression
Assertion	mndmgm	$$⊢M\in \mathrm{Mnd}\to M\in \mathrm{Mgm}$$

Proof

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