This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pnpncand

Description: Addition/subtraction cancellation law. (Contributed by Scott Fenton, 14-Dec-2017)

Ref Expression
Hypotheses pnpncand.1 ⊢ φ → A ∈ ℂ
pnpncand.2 ⊢ φ → B ∈ ℂ
pnpncand.3 ⊢ φ → C ∈ ℂ
Assertion pnpncand ⊢ φ → A + B − C + C − B = A

Proof

Step Hyp Ref Expression
1 pnpncand.1 ⊢ φ → A ∈ ℂ
2 pnpncand.2 ⊢ φ → B ∈ ℂ
3 pnpncand.3 ⊢ φ → C ∈ ℂ
4 2 3 subcld ⊢ φ → B − C ∈ ℂ
5 1 4 addcld ⊢ φ → A + B - C ∈ ℂ
6 5 2 3 subsub2d ⊢ φ → A + B − C - B − C = A + B − C + C − B
7 1 4 pncand ⊢ φ → A + B − C - B − C = A
8 6 7 eqtr3d ⊢ φ → A + B − C + C − B = A