Metamath Proof Explorer


Theorem add1p1

Description: Adding two times 1 to a number. (Contributed by AV, 22-Sep-2018)

Ref Expression
Assertion add1p1 NN+1+1=N+2

Proof

Step Hyp Ref Expression
1 id NN
2 1cnd N1
3 1 2 2 addassd NN+1+1=N+1+1
4 1p1e2 1+1=2
5 4 a1i N1+1=2
6 5 oveq2d NN+1+1=N+2
7 3 6 eqtrd NN+1+1=N+2