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

Metamath Proof Explorer

Theorem submcmn

Description: A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypothesis subgabl.h ⊢ H = G ↾ 𝑠 S
Assertion submcmn ⊢ G ∈ CMnd ∧ S ∈ SubMnd ⁡ G → H ∈ CMnd

Proof

Step Hyp Ref Expression
1 subgabl.h ⊢ H = G ↾ 𝑠 S
2 1 submmnd ⊢ S ∈ SubMnd ⁡ G → H ∈ Mnd
3 1 subcmn ⊢ G ∈ CMnd ∧ H ∈ Mnd → H ∈ CMnd
4 2 3 sylan2 ⊢ G ∈ CMnd ∧ S ∈ SubMnd ⁡ G → H ∈ CMnd