Description: Lemma for dalaw . Special case of dath2 , where C is replaced by ( ( P .\/ S ) ./\ ( Q .\/ T ) ) . The remaining lemmas will eliminate the conditions on the atoms imposed by dath2 . (Contributed by NM, 6-Oct-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dalawlem.l | |
|
dalawlem.j | |
||
dalawlem.m | |
||
dalawlem.a | |
||
dalawlem.o | |
||
Assertion | dalawlem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dalawlem.l | |
|
2 | dalawlem.j | |
|
3 | dalawlem.m | |
|
4 | dalawlem.a | |
|
5 | dalawlem.o | |
|
6 | simp11 | |
|
7 | 6 | hllatd | |
8 | simp121 | |
|
9 | simp131 | |
|
10 | eqid | |
|
11 | 10 2 4 | hlatjcl | |
12 | 6 8 9 11 | syl3anc | |
13 | simp122 | |
|
14 | simp132 | |
|
15 | 10 2 4 | hlatjcl | |
16 | 6 13 14 15 | syl3anc | |
17 | 10 3 | latmcl | |
18 | 7 12 16 17 | syl3anc | |
19 | 6 18 | jca | |
20 | simp12 | |
|
21 | simp13 | |
|
22 | simp2l | |
|
23 | simp2r | |
|
24 | simp31 | |
|
25 | simp32 | |
|
26 | 10 1 3 | latmle1 | |
27 | 7 12 16 26 | syl3anc | |
28 | 10 1 3 | latmle2 | |
29 | 7 12 16 28 | syl3anc | |
30 | simp33 | |
|
31 | 27 29 30 | 3jca | |
32 | eqid | |
|
33 | eqid | |
|
34 | eqid | |
|
35 | 10 1 2 4 3 5 32 33 34 | dath2 | |
36 | 19 20 21 22 23 24 25 31 35 | syl323anc | |