Metamath Proof Explorer

Theorem simpggrpd

Description: A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypothesis simpggrpd.1 
|- ( ph -> G e. SimpGrp )
Assertion simpggrpd 
|- ( ph -> G e. Grp )

Proof

Step Hyp Ref Expression
1 simpggrpd.1 
 |-  ( ph -> G e. SimpGrp )
2 simpggrp 
 |-  ( G e. SimpGrp -> G e. Grp )
3 1 2 syl 
 |-  ( ph -> G e. Grp )