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