Description: Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | atlene.l | |
|
atlene.j | |
||
atlene.a | |
||
Assertion | atleneN | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | atlene.l | |
|
2 | atlene.j | |
|
3 | atlene.a | |
|
4 | eqid | |
|
5 | 1 2 4 3 | atcvrj1 | |
6 | 2 4 3 | atcvrneN | |
7 | 5 6 | syld3an3 | |