Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma. D represents s_2. (Contributed by NM, 18-Nov-2012) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemeda.l | |
|
cdlemeda.j | |
||
cdlemeda.m | |
||
cdlemeda.a | |
||
cdlemeda.h | |
||
cdlemeda.d | |
||
cdlemednu.u | |
||
Assertion | cdlemednuN | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemeda.l | |
|
2 | cdlemeda.j | |
|
3 | cdlemeda.m | |
|
4 | cdlemeda.a | |
|
5 | cdlemeda.h | |
|
6 | cdlemeda.d | |
|
7 | cdlemednu.u | |
|
8 | 1 2 3 4 5 6 | cdlemednpq | |
9 | simp1l | |
|
10 | simp1r | |
|
11 | simp21 | |
|
12 | simp22 | |
|
13 | 1 2 3 4 5 7 | cdlemeulpq | |
14 | 9 10 11 12 13 | syl22anc | |
15 | breq1 | |
|
16 | 14 15 | syl5ibrcom | |
17 | 16 | necon3bd | |
18 | 8 17 | mpd | |