Metamath Proof Explorer

Theorem simpggrp

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

Ref Expression
Assertion simpggrp 
|- ( G e. SimpGrp -> G e. Grp )

Proof

Step Hyp Ref Expression
1 issimpg 
 |-  ( G e. SimpGrp <-> ( G e. Grp /\ ( NrmSGrp ` G ) ~~ 2o ) )
2 1 simplbi 
 |-  ( G e. SimpGrp -> G e. Grp )