Theorem subsubadd23

Description: Swap the second and the third terms in a difference 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	subsubadd23	$$⊢\phi \to A-B-\left(C+D\right)=A-C-\left(B+D\right)$$

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 3	sub32d	$$⊢\phi \to A-B-C=A-C-B$$
6	5	oveq1d	$$⊢\phi \to \left(A-B\right)-C-D=\left(A-C\right)-B-D$$
7	1 2	subcld	$$⊢\phi \to A-B\in ℂ$$
8	7 3 4	subsub4d	$$⊢\phi \to \left(A-B\right)-C-D=A-B-\left(C+D\right)$$
9	1 3	subcld	$$⊢\phi \to A-C\in ℂ$$
10	9 2 4	subsub4d	$$⊢\phi \to \left(A-C\right)-B-D=A-C-\left(B+D\right)$$
11	6 8 10	3eqtr3d	$$⊢\phi \to A-B-\left(C+D\right)=A-C-\left(B+D\right)$$