Theorem addsubsub23

Description: Swap the second and the third terms in a difference of a sum and a difference (or, vice versa, in a sum of a difference and a sum). (Contributed by AV, 15-Nov-2025)

	Ref	Expression
Hypotheses	negidd.1	$$⊢\phi \to A\in ℂ$$
	pncand.2	$$⊢\phi \to B\in ℂ$$
	subaddd.3	$$⊢\phi \to C\in ℂ$$
	addsub4d.4	$$⊢\phi \to D\in ℂ$$
Assertion	addsubsub23	$$⊢\phi \to A+B-\left(C-D\right)=\left(A-C\right)+B+D$$

Proof

Step	Hyp	Ref	Expression
1		negidd.1	$$⊢\phi \to A\in ℂ$$
2		pncand.2	$$⊢\phi \to B\in ℂ$$
3		subaddd.3	$$⊢\phi \to C\in ℂ$$
4		addsub4d.4	$$⊢\phi \to D\in ℂ$$
5	1 2	addcld	$$⊢\phi \to A+B\in ℂ$$
6	5 3 4	subsubd	$$⊢\phi \to A+B-\left(C-D\right)=\left(A+B\right)-C+D$$
7	1 2 3	addsubd	$$⊢\phi \to A+B-C=A-C+B$$
8	7	oveq1d	$$⊢\phi \to \left(A+B\right)-C+D=\left(A-C\right)+B+D$$
9	1 3	subcld	$$⊢\phi \to A-C\in ℂ$$
10	9 2 4	addassd	$$⊢\phi \to \left(A-C\right)+B+D=\left(A-C\right)+B+D$$
11	6 8 10	3eqtrd	$$⊢\phi \to A+B-\left(C-D\right)=\left(A-C\right)+B+D$$