Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mgm2nsgrplem2 Structured version   Unicode version

Theorem mgm2nsgrplem2 16251
 Description: Lemma 2 for mgm2nsgrp 16254. (Contributed by AV, 27-Jan-2020.)
Hypotheses
Ref Expression
mgm2nsgrp.s
mgm2nsgrp.b
mgm2nsgrp.o
mgm2nsgrp.p
Assertion
Ref Expression
mgm2nsgrplem2
Distinct variable groups:   ,,   ,,   ,,   ,   , ,
Allowed substitution hints:   ()   (,)   (,)

Proof of Theorem mgm2nsgrplem2
StepHypRef Expression
1 prid1g 4075 . . 3
2 mgm2nsgrp.s . . 3
31, 2syl6eleqr 2499 . 2
4 prid2g 4076 . . 3
54, 2syl6eleqr 2499 . 2
6 mgm2nsgrp.p . . . . 5
7 mgm2nsgrp.o . . . . 5
86, 7eqtri 2429 . . . 4
98a1i 11 . . 3
10 ifeq1 3886 . . . . . . 7
11 ifid 3919 . . . . . . 7
1210, 11syl6eq 2457 . . . . . 6
1312a1d 25 . . . . 5
14 eqeq1 2404 . . . . . . . . . . 11
1514bicomd 201 . . . . . . . . . 10
1615notbid 292 . . . . . . . . 9
1716biimpac 484 . . . . . . . 8
1817intnand 915 . . . . . . 7
1918iffalsed 3893 . . . . . 6
2019ex 432 . . . . 5
2113, 20pm2.61i 164 . . . 4