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

Metamath Proof Explorer

Theorem mndsgrp

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

Ref Expression
Assertion mndsgrp ⊢ G ∈ Mnd → G ∈ Smgrp

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base G = Base G
2 eqid ⊢ + G = + G
3 1 2 ismnddef ⊢ G ∈ Mnd ↔ G ∈ Smgrp ∧ ∃ e ∈ Base G ∀ x ∈ Base G e + G x = x ∧ x + G e = x
4 3 simplbi ⊢ G ∈ Mnd → G ∈ Smgrp