Metamath Proof Explorer

Theorem 2addsub

Description: Law for subtraction and addition. (Contributed by NM, 20-Nov-2005)

Ref Expression
Assertion 2addsub ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B + C - D = A + C - D + B

Proof

Step Hyp Ref Expression
1 add32 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B + C = A + C + B
2 1 3expa ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B + C = A + C + B
3 2 adantrr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B + C = A + C + B
4 3 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B + C - D = A + C + B - D
5 addcl ⊢ A ∈ ℂ ∧ C ∈ ℂ → A + C ∈ ℂ
6 addsub ⊢ A + C ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ → A + C + B - D = A + C - D + B
7 6 3expb ⊢ A + C ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ → A + C + B - D = A + C - D + B
8 5 7 sylan ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ → A + C + B - D = A + C - D + B
9 8 an4s ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + C + B - D = A + C - D + B
10 4 9 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B + C - D = A + C - D + B