Description: Lemma for dath . Analogue of dalem45 for I G . (Contributed by NM, 16-Aug-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dalem.ph | |
|
dalem.l | |
||
dalem.j | |
||
dalem.a | |
||
dalem.ps | |
||
dalem44.m | |
||
dalem44.o | |
||
dalem44.y | |
||
dalem44.z | |
||
dalem44.g | |
||
dalem44.h | |
||
dalem44.i | |
||
Assertion | dalem47 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dalem.ph | |
|
2 | dalem.l | |
|
3 | dalem.j | |
|
4 | dalem.a | |
|
5 | dalem.ps | |
|
6 | dalem44.m | |
|
7 | dalem44.o | |
|
8 | dalem44.y | |
|
9 | dalem44.z | |
|
10 | dalem44.g | |
|
11 | dalem44.h | |
|
12 | dalem44.i | |
|
13 | 1 2 3 4 8 9 | dalemrot | |
14 | 13 | 3ad2ant1 | |
15 | 1 2 3 4 8 9 | dalemrotyz | |
16 | 15 | 3adant3 | |
17 | 1 2 3 4 5 8 | dalemrotps | |
18 | 17 | 3adant2 | |
19 | biid | |
|
20 | biid | |
|
21 | eqid | |
|
22 | eqid | |
|
23 | 19 2 3 4 20 6 7 21 22 11 12 10 | dalem46 | |
24 | 14 16 18 23 | syl3anc | |