Description: Part of proof of Lemma N of Crawley p. 121 line 37. (Contributed by NM, 27-Feb-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemn11a.b | |
|
cdlemn11a.l | |
||
cdlemn11a.j | |
||
cdlemn11a.a | |
||
cdlemn11a.h | |
||
cdlemn11a.p | |
||
cdlemn11a.o | |
||
cdlemn11a.t | |
||
cdlemn11a.r | |
||
cdlemn11a.e | |
||
cdlemn11a.i | |
||
cdlemn11a.J | |
||
cdlemn11a.u | |
||
cdlemn11a.d | |
||
cdlemn11a.s | |
||
cdlemn11a.f | |
||
cdlemn11a.g | |
||
Assertion | cdlemn11a | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemn11a.b | |
|
2 | cdlemn11a.l | |
|
3 | cdlemn11a.j | |
|
4 | cdlemn11a.a | |
|
5 | cdlemn11a.h | |
|
6 | cdlemn11a.p | |
|
7 | cdlemn11a.o | |
|
8 | cdlemn11a.t | |
|
9 | cdlemn11a.r | |
|
10 | cdlemn11a.e | |
|
11 | cdlemn11a.i | |
|
12 | cdlemn11a.J | |
|
13 | cdlemn11a.u | |
|
14 | cdlemn11a.d | |
|
15 | cdlemn11a.s | |
|
16 | cdlemn11a.f | |
|
17 | cdlemn11a.g | |
|
18 | simp1 | |
|
19 | 2 4 5 6 | lhpocnel2 | |
20 | 19 | 3ad2ant1 | |
21 | simp22 | |
|
22 | 2 4 5 8 17 | ltrniotacl | |
23 | 18 20 21 22 | syl3anc | |
24 | fvresi | |
|
25 | 23 24 | syl | |
26 | 25 | eqcomd | |
27 | 5 8 10 | tendoidcl | |
28 | 27 | 3ad2ant1 | |
29 | riotaex | |
|
30 | 17 29 | eqeltri | |
31 | 8 | fvexi | |
32 | resiexg | |
|
33 | 31 32 | ax-mp | |
34 | 2 4 5 6 8 10 12 17 30 33 | dicopelval2 | |
35 | 18 21 34 | syl2anc | |
36 | 26 28 35 | mpbir2and | |