Description: Lemma for dath . Analogue of dalem57 for E . (Contributed by NM, 10-Aug-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dalem.ph | |
|
dalem.l | |
||
dalem.j | |
||
dalem.a | |
||
dalem.ps | |
||
dalem58.m | |
||
dalem58.o | |
||
dalem58.y | |
||
dalem58.z | |
||
dalem58.e | |
||
dalem58.g | |
||
dalem58.h | |
||
dalem58.i | |
||
dalem58.b1 | |
||
Assertion | dalem58 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dalem.ph | |
|
2 | dalem.l | |
|
3 | dalem.j | |
|
4 | dalem.a | |
|
5 | dalem.ps | |
|
6 | dalem58.m | |
|
7 | dalem58.o | |
|
8 | dalem58.y | |
|
9 | dalem58.z | |
|
10 | dalem58.e | |
|
11 | dalem58.g | |
|
12 | dalem58.h | |
|
13 | dalem58.i | |
|
14 | dalem58.b1 | |
|
15 | 1 2 3 4 8 9 | dalemrot | |
16 | 15 | 3ad2ant1 | |
17 | 1 2 3 4 8 9 | dalemrotyz | |
18 | 17 | 3adant3 | |
19 | 1 2 3 4 5 8 | dalemrotps | |
20 | 19 | 3adant2 | |
21 | biid | |
|
22 | biid | |
|
23 | eqid | |
|
24 | eqid | |
|
25 | eqid | |
|
26 | 21 2 3 4 22 6 7 23 24 10 12 13 11 25 | dalem57 | |
27 | 16 18 20 26 | syl3anc | |
28 | 1 | dalemkehl | |
29 | 28 | 3ad2ant1 | |
30 | 1 2 3 4 5 6 7 8 9 12 | dalem29 | |
31 | 1 2 3 4 5 6 7 8 9 13 | dalem34 | |
32 | 1 2 3 4 5 6 7 8 9 11 | dalem23 | |
33 | 3 4 | hlatjrot | |
34 | 29 30 31 32 33 | syl13anc | |
35 | 1 3 4 | dalemqrprot | |
36 | 35 8 | eqtr4di | |
37 | 36 | 3ad2ant1 | |
38 | 34 37 | oveq12d | |
39 | 38 14 | eqtr4di | |
40 | 27 39 | breqtrd | |