Description: Part of Lemma E in Crawley p. 113. TODO: fix comment. (Contributed by NM, 11-Apr-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdleme.l | |
|
cdleme.a | |
||
cdleme.h | |
||
cdleme.t | |
||
Assertion | cdleme50ex | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdleme.l | |
|
2 | cdleme.a | |
|
3 | cdleme.h | |
|
4 | cdleme.t | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | eqid | |
|
8 | eqid | |
|
9 | eqid | |
|
10 | eqid | |
|
11 | eqid | |
|
12 | 5 1 6 7 2 3 8 9 10 11 4 | cdleme50ltrn | |
13 | 5 1 6 7 2 3 8 9 10 11 | cdleme17d | |
14 | fveq1 | |
|
15 | 14 | eqeq1d | |
16 | 15 | rspcev | |
17 | 12 13 16 | syl2anc | |