Metamath Proof Explorer


Theorem cyggrp

Description: A cyclic group is a group. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Assertion cyggrp GCycGrpGGrp

Proof

Step Hyp Ref Expression
1 eqid BaseG=BaseG
2 eqid G=G
3 1 2 iscyg GCycGrpGGrpxBaseGrannnGx=BaseG
4 3 simplbi GCycGrpGGrp