Theorem pncan2

Description: Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005)

	Ref	Expression
Assertion	pncan2	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B-A=B$$

Proof

Step	Hyp	Ref	Expression
1		addcom	$$⊢\left(B\in ℂ\wedge A\in ℂ\right)\to B+A=A+B$$
2	1	oveq1d	$$⊢\left(B\in ℂ\wedge A\in ℂ\right)\to B+A-A=A+B-A$$
3		pncan	$$⊢\left(B\in ℂ\wedge A\in ℂ\right)\to B+A-A=B$$
4	2 3	eqtr3d	$$⊢\left(B\in ℂ\wedge A\in ℂ\right)\to A+B-A=B$$
5	4	ancoms	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B-A=B$$