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