Metamath Proof Explorer

Theorem subadd4

Description: Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 24-Aug-2006)

Ref Expression
Assertion subadd4 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧D∈ℂ→A-B-C−D=A+D-B+C

Proof

Step Hyp Ref Expression
1 subcl ⊢A∈ℂ∧B∈ℂ→A−B∈ℂ
2 subsub2 ⊢A−B∈ℂ∧C∈ℂ∧D∈ℂ→A-B-C−D=A−B+D-C
3 2 3expb ⊢A−B∈ℂ∧C∈ℂ∧D∈ℂ→A-B-C−D=A−B+D-C
4 1 3 sylan ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧D∈ℂ→A-B-C−D=A−B+D-C
5 addsub4 ⊢A∈ℂ∧D∈ℂ∧B∈ℂ∧C∈ℂ→A+D-B+C=A−B+D-C
6 5 an42s ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧D∈ℂ→A+D-B+C=A−B+D-C
7 4 6 eqtr4d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧D∈ℂ→A-B-C−D=A+D-B+C