Description: Obsolete version of sgrpmgm as of 3-Feb-2020. A semigroup is a magma. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | smgrpismgmOLD | ⊢ ( 𝐺 ∈ SemiGrp → 𝐺 ∈ Magma ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elin | ⊢ ( 𝐺 ∈ ( Magma ∩ Ass ) ↔ ( 𝐺 ∈ Magma ∧ 𝐺 ∈ Ass ) ) | |
| 2 | 1 | simplbi | ⊢ ( 𝐺 ∈ ( Magma ∩ Ass ) → 𝐺 ∈ Magma ) |
| 3 | df-sgrOLD | ⊢ SemiGrp = ( Magma ∩ Ass ) | |
| 4 | 2 3 | eleq2s | ⊢ ( 𝐺 ∈ SemiGrp → 𝐺 ∈ Magma ) |