Theorem nncan

Description: Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

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

Proof

Step	Hyp	Ref	Expression
1		subsub2	$$⊢\left(A\in ℂ\wedge A\in ℂ\wedge B\in ℂ\right)\to A-\left(A-B\right)=A+B-A$$
2	1	3anidm12	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A-\left(A-B\right)=A+B-A$$
3		pncan3	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B-A=B$$
4	2 3	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A-\left(A-B\right)=B$$