Metamath Proof Explorer


Theorem subggrp

Description: A subgroup is a group. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypothesis subggrp.h H=G𝑠S
Assertion subggrp SSubGrpGHGrp

Proof

Step Hyp Ref Expression
1 subggrp.h H=G𝑠S
2 eqid BaseG=BaseG
3 2 issubg SSubGrpGGGrpSBaseGG𝑠SGrp
4 3 simp3bi SSubGrpGG𝑠SGrp
5 1 4 eqeltrid SSubGrpGHGrp