Description: An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | atcvr1.j | |
|
atcvr1.c | |
||
atcvr1.a | |
||
Assertion | atcvr1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | atcvr1.j | |
|
2 | atcvr1.c | |
|
3 | atcvr1.a | |
|
4 | hlomcmcv | |
|
5 | 1 2 3 | cvlatcvr1 | |
6 | 4 5 | syl3an1 | |