Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme11 . (Contributed by NM, 15-Jun-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdleme12.l | |
|
cdleme12.j | |
||
cdleme12.m | |
||
cdleme12.a | |
||
cdleme12.h | |
||
cdleme12.u | |
||
cdleme12.f | |
||
cdleme12.g | |
||
Assertion | cdleme11l | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdleme12.l | |
|
2 | cdleme12.j | |
|
3 | cdleme12.m | |
|
4 | cdleme12.a | |
|
5 | cdleme12.h | |
|
6 | cdleme12.u | |
|
7 | cdleme12.f | |
|
8 | cdleme12.g | |
|
9 | simp11 | |
|
10 | simp12 | |
|
11 | simp13l | |
|
12 | simp21 | |
|
13 | simp22l | |
|
14 | simp23l | |
|
15 | simp23r | |
|
16 | simp31 | |
|
17 | simp33 | |
|
18 | eqid | |
|
19 | eqid | |
|
20 | 1 2 3 4 5 6 18 19 | cdleme11e | |
21 | 9 10 11 12 13 14 15 16 17 20 | syl333anc | |
22 | oveq2 | |
|
23 | 22 | oveq1d | |
24 | 23 | adantl | |
25 | simp13 | |
|
26 | 1 2 3 4 5 6 18 6 7 | cdleme11k | |
27 | 9 10 25 12 14 16 26 | syl132anc | |
28 | 27 | adantr | |
29 | simp22 | |
|
30 | simp32 | |
|
31 | 1 2 3 4 5 6 19 6 8 | cdleme11k | |
32 | 9 10 25 29 14 30 31 | syl132anc | |
33 | 32 | adantr | |
34 | 24 28 33 | 3eqtr4d | |
35 | 34 | ex | |
36 | 35 | necon3d | |
37 | 21 36 | mpd | |