Metamath Proof Explorer

Theorem mndoismgmOLD

Description: Obsolete version of mndmgm as of 3-Feb-2020. A monoid is a magma. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion mndoismgmOLD 
|- ( G e. MndOp -> G e. Magma )

Proof

Step Hyp Ref Expression
1 mndoissmgrpOLD 
 |-  ( G e. MndOp -> G e. SemiGrp )
2 smgrpismgmOLD 
 |-  ( G e. SemiGrp -> G e. Magma )
3 1 2 syl 
 |-  ( G e. MndOp -> G e. Magma )