Metamath Proof Explorer

Theorem simpggrp

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

Ref Expression
Assertion simpggrp ⊢ G ∈ SimpGrp → G ∈ Grp

Proof

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