Description: A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | cmnmndd.1 | ⊢ ( 𝜑 → 𝐺 ∈ CMnd ) | |
Assertion | cmnmndd | ⊢ ( 𝜑 → 𝐺 ∈ Mnd ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmnmndd.1 | ⊢ ( 𝜑 → 𝐺 ∈ CMnd ) | |
2 | cmnmnd | ⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd ) | |
3 | 1 2 | syl | ⊢ ( 𝜑 → 𝐺 ∈ Mnd ) |