Theorem assraddsubi

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

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

Proof

Step	Hyp	Ref	Expression
1		assraddsubi.1	|- B e. CC
2		assraddsubi.2	|- C e. CC
3		assraddsubi.3	|- D e. CC
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 ) )