Theorem assraddsubd

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

	Ref	Expression
Hypotheses	assraddsubd.1	|- ( ph -> B e. CC )
	assraddsubd.2	|- ( ph -> C e. CC )
	assraddsubd.3	|- ( ph -> D e. CC )
	assraddsubd.4	|- ( ph -> A = ( ( B + C ) - D ) )
Assertion	assraddsubd	|- ( ph -> A = ( B + ( C - D ) ) )

Proof

Step	Hyp	Ref	Expression
1		assraddsubd.1	|- ( ph -> B e. CC )
2		assraddsubd.2	|- ( ph -> C e. CC )
3		assraddsubd.3	|- ( ph -> D e. CC )
4		assraddsubd.4	|- ( ph -> A = ( ( B + C ) - D ) )
5	1 2 3	addsubassd	|- ( ph -> ( ( B + C ) - D ) = ( B + ( C - D ) ) )
6	4 5	eqtrd	|- ( ph -> A = ( B + ( C - D ) ) )