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 \in CMnd \land S \in SubMnd (G)) \to H \in CMnd$

Step	Hyp	Ref	Expression
1		subgabl.h	$⊢ H = G ↾_{𝑠} S$
2	1	submmnd	$⊢ S \in SubMnd (G) \to H \in Mnd$
3	1	subcmn	$⊢ (G \in CMnd \land H \in Mnd) \to H \in CMnd$
4	2 3	sylan2	$⊢ (G \in CMnd \land S \in SubMnd (G)) \to H \in CMnd$