Metamath Proof Explorer


Theorem pnpncand

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

Ref Expression
Hypotheses pnpncand.1 ( 𝜑𝐴 ∈ ℂ )
pnpncand.2 ( 𝜑𝐵 ∈ ℂ )
pnpncand.3 ( 𝜑𝐶 ∈ ℂ )
Assertion pnpncand ( 𝜑 → ( ( 𝐴 + ( 𝐵𝐶 ) ) + ( 𝐶𝐵 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 pnpncand.1 ( 𝜑𝐴 ∈ ℂ )
2 pnpncand.2 ( 𝜑𝐵 ∈ ℂ )
3 pnpncand.3 ( 𝜑𝐶 ∈ ℂ )
4 2 3 subcld ( 𝜑 → ( 𝐵𝐶 ) ∈ ℂ )
5 1 4 addcld ( 𝜑 → ( 𝐴 + ( 𝐵𝐶 ) ) ∈ ℂ )
6 5 2 3 subsub2d ( 𝜑 → ( ( 𝐴 + ( 𝐵𝐶 ) ) − ( 𝐵𝐶 ) ) = ( ( 𝐴 + ( 𝐵𝐶 ) ) + ( 𝐶𝐵 ) ) )
7 1 4 pncand ( 𝜑 → ( ( 𝐴 + ( 𝐵𝐶 ) ) − ( 𝐵𝐶 ) ) = 𝐴 )
8 6 7 eqtr3d ( 𝜑 → ( ( 𝐴 + ( 𝐵𝐶 ) ) + ( 𝐶𝐵 ) ) = 𝐴 )