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 ∈ SimpGrp → NrmSGrp ⁡ G ≈ 2 𝑜

Proof

Step Hyp Ref Expression
1 issimpg ⊢ G ∈ SimpGrp ↔ G ∈ Grp ∧ NrmSGrp ⁡ G ≈ 2 𝑜
2 1 simprbi ⊢ G ∈ SimpGrp → NrmSGrp ⁡ G ≈ 2 𝑜