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