Theorem ablgrp

Description: An Abelian group is a group. (Contributed by NM, 26-Aug-2011)

	Ref	Expression
Assertion	ablgrp	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )

Proof

Step	Hyp	Ref	Expression
1		isabl	⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd ) )
2	1	simplbi	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )