This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpsgrp

Description: A group is a semigroup. (Contributed by AV, 28-Aug-2021)

Ref Expression
Assertion grpsgrp 
|- ( G e. Grp -> G e. Smgrp )

Proof

Step Hyp Ref Expression
1 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
2 mndsgrp 
 |-  ( G e. Mnd -> G e. Smgrp )
3 1 2 syl 
 |-  ( G e. Grp -> G e. Smgrp )