Theorem subsub3

Description: Law for double subtraction. (Contributed by NM, 27-Jul-2005)

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

Proof

Step	Hyp	Ref	Expression
1		subsub2	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge C\in ℂ\right)\to A-\left(B-C\right)=A+C-B$$
2		addsubass	$$⊢\left(A\in ℂ\wedge C\in ℂ\wedge B\in ℂ\right)\to A+C-B=A+C-B$$
3	2	3com23	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge C\in ℂ\right)\to A+C-B=A+C-B$$
4	1 3	eqtr4d	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge C\in ℂ\right)\to A-\left(B-C\right)=A+C-B$$