Metamath Proof Explorer

Theorem simpg2nsg

Description: A simple group has two normal subgroups. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Assertion simpg2nsg 
|- ( G e. SimpGrp -> ( NrmSGrp ` G ) ~~ 2o )

Proof

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