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

Metamath Proof Explorer

Theorem sgrpmgm

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

Ref Expression
Assertion sgrpmgm ⊢ M ∈ Smgrp → M ∈ Mgm

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base M = Base M
2 eqid ⊢ + M = + M
3 1 2 issgrp ⊢ M ∈ Smgrp ↔ M ∈ Mgm ∧ ∀ x ∈ Base M ∀ y ∈ Base M ∀ z ∈ Base M x + M y + M z = x + M y + M z
4 3 simplbi ⊢ M ∈ Smgrp → M ∈ Mgm