Theorem assraddsubd

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

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

Proof

Step	Hyp	Ref	Expression
1		assraddsubd.1	$$⊢\phi \to B\in ℂ$$
2		assraddsubd.2	$$⊢\phi \to C\in ℂ$$
3		assraddsubd.3	$$⊢\phi \to D\in ℂ$$
4		assraddsubd.4	$$⊢\phi \to A=B+C-D$$
5	1 2 3	addsubassd	$$⊢\phi \to B+C-D=B+C-D$$
6	4 5	eqtrd	$$⊢\phi \to A=B+C-D$$