Metamath Proof Explorer


Theorem 1p1times

Description: Two times a number. (Contributed by NM, 18-May-1999) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion 1p1times A1+1A=A+A

Proof

Step Hyp Ref Expression
1 1cnd A1
2 id AA
3 mullid A1A=A
4 3 3 oveq12d A1A+1A=A+A
5 1 2 1 4 joinlmuladdmuld A1+1A=A+A