Theorem issimpgd

Description: Deduce a simple group from its properties. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	issimpgd.1	$$⊢\phi \to G\in \mathrm{Grp}$$
	issimpgd.2	$$⊢\phi \to \mathrm{NrmSGrp}\left(G\right)\approx 2_{𝑜}$$
Assertion	issimpgd	$$⊢\phi \to G\in \mathrm{SimpGrp}$$

Proof

Step	Hyp	Ref	Expression
1		issimpgd.1	$$⊢\phi \to G\in \mathrm{Grp}$$
2		issimpgd.2	$$⊢\phi \to \mathrm{NrmSGrp}\left(G\right)\approx 2_{𝑜}$$
3		issimpg	$$⊢G\in \mathrm{SimpGrp}\leftrightarrow \left(G\in \mathrm{Grp}\wedge \mathrm{NrmSGrp}\left(G\right)\approx 2_{𝑜}\right)$$
4	1 2 3	sylanbrc	$$⊢\phi \to G\in \mathrm{SimpGrp}$$