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

Metamath Proof Explorer

Theorem grpmndd

Description: A group is a monoid. (Contributed by SN, 1-Jun-2024)

Ref Expression
Hypothesis grpmndd.1 
|- ( ph -> G e. Grp )
Assertion grpmndd 
|- ( ph -> G e. Mnd )

Proof

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