Metamath Proof Explorer

Theorem addsub12

Description: Commutative/associative law for addition and subtraction. (Contributed by NM, 8-Feb-2005)

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

Proof

Step Hyp Ref Expression
1 subadd23 ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A - C + B = A + B - C
2 subcl ⊢ A ∈ ℂ ∧ C ∈ ℂ → A − C ∈ ℂ
3 addcom ⊢ A − C ∈ ℂ ∧ B ∈ ℂ → A - C + B = B + A - C
4 2 3 stoic3 ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A - C + B = B + A - C
5 1 4 eqtr3d ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A + B - C = B + A - C
6 5 3com23 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B - C = B + A - C