This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 e. Mnd -> M e. Mgm )

Proof

Step Hyp Ref Expression
1 mndsgrp 
 |-  ( M e. Mnd -> M e. Smgrp )
2 sgrpmgm 
 |-  ( M e. Smgrp -> M e. Mgm )
3 1 2 syl 
 |-  ( M e. Mnd -> M e. Mgm )