Description: Generalization of 2llnma1 . (Contributed by NM, 26-Apr-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 2llnma1b.b | |
|
2llnma1b.l | |
||
2llnma1b.j | |
||
2llnma1b.m | |
||
2llnma1b.a | |
||
Assertion | 2llnma1b | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2llnma1b.b | |
|
2 | 2llnma1b.l | |
|
3 | 2llnma1b.j | |
|
4 | 2llnma1b.m | |
|
5 | 2llnma1b.a | |
|
6 | hllat | |
|
7 | 6 | 3ad2ant1 | |
8 | simp22 | |
|
9 | 1 5 | atbase | |
10 | 8 9 | syl | |
11 | simp21 | |
|
12 | 1 2 3 | latlej1 | |
13 | 7 10 11 12 | syl3anc | |
14 | simp23 | |
|
15 | 1 5 | atbase | |
16 | 14 15 | syl | |
17 | 1 2 3 | latlej1 | |
18 | 7 10 16 17 | syl3anc | |
19 | 1 3 | latjcl | |
20 | 7 10 11 19 | syl3anc | |
21 | simp1 | |
|
22 | 1 3 5 | hlatjcl | |
23 | 21 8 14 22 | syl3anc | |
24 | 1 2 4 | latlem12 | |
25 | 7 10 20 23 24 | syl13anc | |
26 | 13 18 25 | mpbi2and | |
27 | hlatl | |
|
28 | 27 | 3ad2ant1 | |
29 | simp3 | |
|
30 | nbrne2 | |
|
31 | 13 29 30 | syl2anc | |
32 | 1 3 | latjcl | |
33 | 7 20 16 32 | syl3anc | |
34 | 1 2 3 | latlej1 | |
35 | 7 20 16 34 | syl3anc | |
36 | 1 2 7 10 20 33 13 35 | lattrd | |
37 | 1 2 3 4 5 | cvrat3 | |
38 | 37 | 3impia | |
39 | 21 20 8 14 31 29 36 38 | syl133anc | |
40 | 2 5 | atcmp | |
41 | 28 8 39 40 | syl3anc | |
42 | 26 41 | mpbid | |
43 | 42 | eqcomd | |