Description: Lemma for 3at . (Contributed by NM, 23-Jun-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 3at.l | |
|
3at.j | |
||
3at.a | |
||
Assertion | 3atlem5 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3at.l | |
|
2 | 3at.j | |
|
3 | 3at.a | |
|
4 | oveq2 | |
|
5 | 4 | eqcoms | |
6 | 5 | breq2d | |
7 | 5 | eqeq2d | |
8 | 6 7 | imbi12d | |
9 | simp1l | |
|
10 | simp1r1 | |
|
11 | simp2 | |
|
12 | simp1r3 | |
|
13 | simp3 | |
|
14 | 1 2 3 | 3atlem3 | |
15 | 9 10 11 12 13 14 | syl131anc | |
16 | 15 | 3expia | |
17 | simp11 | |
|
18 | simp123 | |
|
19 | simp122 | |
|
20 | simp121 | |
|
21 | 18 19 20 | 3jca | |
22 | simp131 | |
|
23 | simp132 | |
|
24 | 22 23 | jca | |
25 | simp21 | |
|
26 | simp22 | |
|
27 | 1 2 3 | hlatexch2 | |
28 | 17 20 18 19 26 27 | syl131anc | |
29 | 25 28 | mtod | |
30 | 17 | hllatd | |
31 | eqid | |
|
32 | 31 3 | atbase | |
33 | 18 32 | syl | |
34 | 31 3 | atbase | |
35 | 20 34 | syl | |
36 | 31 3 | atbase | |
37 | 19 36 | syl | |
38 | 31 1 2 | latnlej1r | |
39 | 30 33 35 37 25 38 | syl131anc | |
40 | simp3 | |
|
41 | 1 2 3 | 3atlem4 | |
42 | 17 21 24 29 39 40 41 | syl321anc | |
43 | 42 | 3expia | |
44 | simpl1 | |
|
45 | 44 | hllatd | |
46 | simpl21 | |
|
47 | 46 34 | syl | |
48 | simpl22 | |
|
49 | 48 36 | syl | |
50 | simpl23 | |
|
51 | 50 32 | syl | |
52 | 31 2 | latj31 | |
53 | 45 47 49 51 52 | syl13anc | |
54 | 53 | breq1d | |
55 | 53 | eqeq1d | |
56 | 43 54 55 | 3imtr4d | |
57 | 8 16 56 | pm2.61ne | |
58 | 57 | 3impia | |