Metamath Proof Explorer

Theorem subsub

Description: Law for double subtraction. (Contributed by NM, 13-May-2004)

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

Proof

Step Hyp Ref Expression
1 subsub2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B−C=A+C-B
2 addsubass ⊢A∈ℂ∧C∈ℂ∧B∈ℂ→A+C-B=A+C-B
3 addsub ⊢A∈ℂ∧C∈ℂ∧B∈ℂ→A+C-B=A-B+C
4 2 3 eqtr3d ⊢A∈ℂ∧C∈ℂ∧B∈ℂ→A+C-B=A-B+C
5 4 3com23 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+C-B=A-B+C
6 1 5 eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B−C=A-B+C