Description: Atom exchange property. Version of hlatexch2 with covers relation. (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | atexchcvr.j | |
|
atexchcvr.a | |
||
atexchcvr.c | |
||
Assertion | atexchcvrN | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | atexchcvr.j | |
|
2 | atexchcvr.a | |
|
3 | atexchcvr.c | |
|
4 | simpl1 | |
|
5 | simpl21 | |
|
6 | eqid | |
|
7 | 6 2 | atbase | |
8 | 5 7 | syl | |
9 | 4 | hllatd | |
10 | simpl22 | |
|
11 | 6 2 | atbase | |
12 | 10 11 | syl | |
13 | simpl23 | |
|
14 | 6 2 | atbase | |
15 | 13 14 | syl | |
16 | 6 1 | latjcl | |
17 | 9 12 15 16 | syl3anc | |
18 | 4 8 17 | 3jca | |
19 | eqid | |
|
20 | 6 19 3 | cvrle | |
21 | 18 20 | sylancom | |
22 | 21 | ex | |
23 | 19 1 2 | hlatexch2 | |
24 | simpl1 | |
|
25 | simpl22 | |
|
26 | simpl21 | |
|
27 | simpl23 | |
|
28 | simpl3 | |
|
29 | simpr | |
|
30 | 19 1 3 2 | atcvrj2 | |
31 | 24 25 26 27 28 29 30 | syl132anc | |
32 | 31 | ex | |
33 | 22 23 32 | 3syld | |