Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 31-Mar-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdleme31sde.c | |
|
cdleme31sde.e | |
||
cdleme31sde.x | |
||
cdleme31sde.z | |
||
Assertion | cdleme31sde | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdleme31sde.c | |
|
2 | cdleme31sde.e | |
|
3 | cdleme31sde.x | |
|
4 | cdleme31sde.z | |
|
5 | 2 | csbeq2i | |
6 | nfcvd | |
|
7 | oveq1 | |
|
8 | oveq2 | |
|
9 | 8 | oveq1d | |
10 | 9 | oveq2d | |
11 | 7 10 | oveq12d | |
12 | 11 1 3 | 3eqtr4g | |
13 | oveq2 | |
|
14 | 13 | oveq1d | |
15 | 12 14 | oveq12d | |
16 | 15 | oveq2d | |
17 | 6 16 | csbiegf | |
18 | 5 17 | eqtrid | |
19 | 18 | csbeq2dv | |
20 | eqid | |
|
21 | 20 4 | cdleme31se | |
22 | 19 21 | sylan9eqr | |