Metamath Proof Explorer


Theorem subgsubm

Description: A subgroup is a submonoid. (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Assertion subgsubm S SubGrp G S SubMnd G

Proof

Step Hyp Ref Expression
1 subgrcl S SubGrp G G Grp
2 eqid inv g G = inv g G
3 2 issubg3 G Grp S SubGrp G S SubMnd G x S inv g G x S
4 1 3 syl S SubGrp G S SubGrp G S SubMnd G x S inv g G x S
5 4 ibi S SubGrp G S SubMnd G x S inv g G x S
6 5 simpld S SubGrp G S SubMnd G