Description: TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemg4.l | |
|
cdlemg4.a | |
||
cdlemg4.h | |
||
cdlemg4.t | |
||
cdlemg4.r | |
||
cdlemg4.j | |
||
cdlemg4b.v | |
||
cdlemg4.m | |
||
Assertion | cdlemg4f | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemg4.l | |
|
2 | cdlemg4.a | |
|
3 | cdlemg4.h | |
|
4 | cdlemg4.t | |
|
5 | cdlemg4.r | |
|
6 | cdlemg4.j | |
|
7 | cdlemg4b.v | |
|
8 | cdlemg4.m | |
|
9 | 1 2 3 4 5 6 7 8 | cdlemg4e | |
10 | simp1 | |
|
11 | simp21 | |
|
12 | simp23 | |
|
13 | simp31 | |
|
14 | simp33 | |
|
15 | 1 2 3 4 5 | cdlemg4a | |
16 | 10 11 12 13 14 15 | syl131anc | |
17 | 7 16 | eqtr4id | |
18 | 17 | oveq2d | |
19 | simp22 | |
|
20 | 1 2 3 4 5 6 7 | cdlemg4b12 | |
21 | 10 19 13 20 | syl3anc | |
22 | 18 21 | eqtr3d | |
23 | eqid | |
|
24 | 3 4 1 6 2 8 23 | cdlemg2m | |
25 | 10 11 19 13 24 | syl121anc | |
26 | 14 25 | oveq12d | |
27 | 22 26 | oveq12d | |
28 | 9 27 | eqtrd | |