Metamath Proof Explorer

Theorem pnpcan

Description: Cancellation law for mixed addition and subtraction. (Contributed by NM, 4-Mar-2005) (Revised by Mario Carneiro, 27-May-2016) (Proof shortened by SN, 13-Nov-2023)

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

Proof

Step Hyp Ref Expression
1 addcl ⊢A∈ℂ∧B∈ℂ→A+B∈ℂ
2 subsub4 ⊢A+B∈ℂ∧A∈ℂ∧C∈ℂ→A+B-A-C=A+B-A+C
3 1 2 stoic4a ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+B-A-C=A+B-A+C
4 pncan2 ⊢A∈ℂ∧B∈ℂ→A+B-A=B
5 4 3adant3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+B-A=B
6 5 oveq1d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+B-A-C=B−C
7 3 6 eqtr3d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+B-A+C=B−C