Description: Two times a number. (Contributed by NM, 18-May-1999) (Revised by Mario Carneiro, 27-May-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | 1p1times | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1cnd | |
|
2 | id | |
|
3 | mullid | |
|
4 | 3 3 | oveq12d | |
5 | 1 2 1 4 | joinlmuladdmuld | |