Theorem assraddsubi

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

	Ref	Expression
Hypotheses	assraddsubi.1	⊢ 𝐵 ∈ ℂ
	assraddsubi.2	⊢ 𝐶 ∈ ℂ
	assraddsubi.3	⊢ 𝐷 ∈ ℂ
	assraddsubi.4	⊢ 𝐴 = ( ( 𝐵 + 𝐶 ) − 𝐷 )
Assertion	assraddsubi	⊢ 𝐴 = ( 𝐵 + ( 𝐶 − 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		assraddsubi.1	⊢ 𝐵 ∈ ℂ
2		assraddsubi.2	⊢ 𝐶 ∈ ℂ
3		assraddsubi.3	⊢ 𝐷 ∈ ℂ
4		assraddsubi.4	⊢ 𝐴 = ( ( 𝐵 + 𝐶 ) − 𝐷 )
5	1 2 3	addsubassi	⊢ ( ( 𝐵 + 𝐶 ) − 𝐷 ) = ( 𝐵 + ( 𝐶 − 𝐷 ) )
6	4 5	eqtri	⊢ 𝐴 = ( 𝐵 + ( 𝐶 − 𝐷 ) )