Description: Lattice join distributes over itself. (Contributed by NM, 30-Jul-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | latjass.b | |
|
latjass.j | |
||
Assertion | latjjdi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | latjass.b | |
|
2 | latjass.j | |
|
3 | simpr1 | |
|
4 | 1 2 | latjidm | |
5 | 3 4 | syldan | |
6 | 5 | oveq1d | |
7 | simpl | |
|
8 | simpr2 | |
|
9 | simpr3 | |
|
10 | 1 2 | latj4 | |
11 | 7 3 3 8 9 10 | syl122anc | |
12 | 6 11 | eqtr3d | |