Theorem subadd23

Description: Commutative/associative law for addition and subtraction. (Contributed by NM, 1-Feb-2007)

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

Proof

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