Theorem add1p1

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

	Ref	Expression
Assertion	add1p1	$$⊢N\in ℂ\to N+1+1=N+2$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢N\in ℂ\to N\in ℂ$$
2		1cnd	$$⊢N\in ℂ\to 1\in ℂ$$
3	1 2 2	addassd	$$⊢N\in ℂ\to N+1+1=N+1+1$$
4		1p1e2	$$⊢1+1=2$$
5	4	a1i	$$⊢N\in ℂ\to 1+1=2$$
6	5	oveq2d	$$⊢N\in ℂ\to N+1+1=N+2$$
7	3 6	eqtrd	$$⊢N\in ℂ\to N+1+1=N+2$$