Metamath Proof Explorer

Theorem addsub

Description: Law for addition and subtraction. (Contributed by NM, 19-Aug-2001) (Proof shortened by Andrew Salmon, 22-Oct-2011)

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

Proof

Step Hyp Ref Expression
1 addcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B = B + A
2 1 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - C = B + A - C
3 2 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B - C = B + A - C
4 addsubass ⊢ B ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ ℂ → B + A - C = B + A - C
5 4 3com12 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B + A - C = B + A - C
6 subcl ⊢ A ∈ ℂ ∧ C ∈ ℂ → A − C ∈ ℂ
7 addcom ⊢ B ∈ ℂ ∧ A − C ∈ ℂ → B + A - C = A - C + B
8 6 7 sylan2 ⊢ B ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ ℂ → B + A - C = A - C + B
9 8 3impb ⊢ B ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ ℂ → B + A - C = A - C + B
10 9 3com12 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B + A - C = A - C + B
11 3 5 10 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B - C = A - C + B