Theorem assraddsubi

Description: Associate RHS addition-subtraction. (Contributed by David A. Wheeler, 11-Oct-2018)

	Ref	Expression
Hypotheses	assraddsubi.1	$$⊢B\in ℂ$$
	assraddsubi.2	$$⊢C\in ℂ$$
	assraddsubi.3	$$⊢D\in ℂ$$
	assraddsubi.4	$$⊢A=B+C-D$$
Assertion	assraddsubi	$$⊢A=B+C-D$$

Proof

Step	Hyp	Ref	Expression
1		assraddsubi.1	$$⊢B\in ℂ$$
2		assraddsubi.2	$$⊢C\in ℂ$$
3		assraddsubi.3	$$⊢D\in ℂ$$
4		assraddsubi.4	$$⊢A=B+C-D$$
5	1 2 3	addsubassi	$$⊢B+C-D=B+C-D$$
6	4 5	eqtri	$$⊢A=B+C-D$$