Description: Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lplnri1.j | ||
lplnri1.a | |||
lplnri1.p | |||
lplnri1.y | |||
Assertion | lplnri2N |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lplnri1.j | ||
2 | lplnri1.a | ||
3 | lplnri1.p | ||
4 | lplnri1.y | ||
5 | eqid | ||
6 | 5 1 2 3 4 | lplnriaN | |
7 | 5 1 2 | atnlej2 | |
8 | 6 7 | syld3an3 |