Metamath Proof Explorer

Theorem sub32

Description: Swap the second and third terms in a double subtraction. (Contributed by NM, 19-Aug-2005)

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

Proof

Step Hyp Ref Expression
1 addcom ⊢B∈ℂ∧C∈ℂ→B+C=C+B
2 1 3adant1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B+C=C+B
3 2 oveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B+C=A−C+B
4 subsub4 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A-B-C=A−B+C
5 subsub4 ⊢A∈ℂ∧C∈ℂ∧B∈ℂ→A-C-B=A−C+B
6 5 3com23 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A-C-B=A−C+B
7 3 4 6 3eqtr4d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A-B-C=A-C-B