Theorem int-addassocd

Description: AdditionAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		int-addassocd.1	$$⊢\phi \to A\in ℝ$$
2		int-addassocd.2	$$⊢\phi \to C\in ℝ$$
3		int-addassocd.3	$$⊢\phi \to D\in ℝ$$
4		int-addassocd.4	$$⊢\phi \to A=B$$
5	1	recnd	$$⊢\phi \to A\in ℂ$$
6	2	recnd	$$⊢\phi \to C\in ℂ$$
7	3	recnd	$$⊢\phi \to D\in ℂ$$
8	5 6 7	addassd	$$⊢\phi \to A+C+D=A+C+D$$
9	4	oveq1d	$$⊢\phi \to A+C+D=B+C+D$$
10	8 9	eqtr2d	$$⊢\phi \to B+C+D=A+C+D$$