Description: Lemma for 4at . Substitute T for P . (Contributed by NM, 9-Jul-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 4at.l | |
|
4at.j | |
||
4at.a | |
||
Assertion | 4atlem12a | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 4at.l | |
|
2 | 4at.j | |
|
3 | 4at.a | |
|
4 | simp11 | |
|
5 | simp12 | |
|
6 | simp13 | |
|
7 | 4 | hllatd | |
8 | simp21 | |
|
9 | simp22 | |
|
10 | eqid | |
|
11 | 10 2 3 | hlatjcl | |
12 | 4 8 9 11 | syl3anc | |
13 | simp23 | |
|
14 | 10 3 | atbase | |
15 | 13 14 | syl | |
16 | 10 2 | latjcl | |
17 | 7 12 15 16 | syl3anc | |
18 | simp3 | |
|
19 | 10 1 2 3 | hlexchb2 | |
20 | 4 5 6 17 18 19 | syl131anc | |
21 | 1 2 3 | 4atlem4a | |
22 | 4 6 8 9 13 21 | syl32anc | |
23 | 22 | breq2d | |
24 | 1 2 3 | 4atlem4a | |
25 | 4 5 8 9 13 24 | syl32anc | |
26 | 25 22 | eqeq12d | |
27 | 20 23 26 | 3bitr4d | |