Theorem npncan2

Description: Cancellation law for subtraction. (Contributed by Scott Fenton, 21-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		npncan	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge A\in ℂ\right)\to \left(A-B\right)+B-A=A-A$$
2	1	3anidm13	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A-B\right)+B-A=A-A$$
3		subid	$$⊢A\in ℂ\to A-A=0$$
4	3	adantr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A-A=0$$
5	2 4	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A-B\right)+B-A=0$$