Metamath Proof Explorer

Theorem ablgrp

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

Ref Expression
Assertion ablgrp 
|- ( G e. Abel -> G e. Grp )

Proof

Step Hyp Ref Expression
1 isabl 
 |-  ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
2 1 simplbi 
 |-  ( G e. Abel -> G e. Grp )