Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pl42lem4N Structured version   Unicode version

Theorem pl42lem4N 30853
 Description: Lemma for pl42N 30854. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
pl42lem.b
pl42lem.l
pl42lem.j
pl42lem.m
pl42lem.o
pl42lem.f
pl42lem.p
Assertion
Ref Expression
pl42lem4N

Proof of Theorem pl42lem4N
StepHypRef Expression
1 pl42lem.b . . . . 5
2 pl42lem.l . . . . 5
3 pl42lem.j . . . . 5
4 pl42lem.m . . . . 5
5 pl42lem.o . . . . 5
6 pl42lem.f . . . . 5
7 pl42lem.p . . . . 5
81, 2, 3, 4, 5, 6, 7pl42lem1N 30850 . . . 4
983impia 1151 . . 3
101, 2, 3, 4, 5, 6, 7pl42lem3N 30852 . . . . 5
11 simpl1 961 . . . . . . 7
12 hllat 30235 . . . . . . . . 9
1311, 12syl 16 . . . . . . . 8
14 simpl2 962 . . . . . . . 8
15 eqid 2438 . . . . . . . . 9
161, 15, 6pmapsub 30639 . . . . . . . 8
1713, 14, 16syl2anc 644 . . . . . . 7
18 simpl3 963 . . . . . . . 8
191, 15, 6pmapsub 30639 . . . . . . . 8
2013, 18, 19syl2anc 644 . . . . . . 7
21 simpr2 965 . . . . . . . 8
221, 15, 6pmapsub 30639 . . . . . . . 8
2313, 21, 22syl2anc 644 . . . . . . 7
24 simpr3 966 . . . . . . . 8
251, 15, 6pmapsub 30639 . . . . . . . 8
2613, 24, 25syl2anc 644 . . . . . . 7
2715, 7pmodl42N 30722 . . . . . . 7
2811, 17, 20, 23, 26, 27syl32anc 1193 . . . . . 6
291, 2, 3, 4, 5, 6, 7pl42lem2N 30851 . . . . . 6
3028, 29eqsstrd 3384 . . . . 5
3110, 30sstrd 3360 . . . 4