Metamath Proof Explorer


Theorem pnpncand

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

Ref Expression
Hypotheses pnpncand.1
|- ( ph -> A e. CC )
pnpncand.2
|- ( ph -> B e. CC )
pnpncand.3
|- ( ph -> C e. CC )
Assertion pnpncand
|- ( ph -> ( ( A + ( B - C ) ) + ( C - B ) ) = A )

Proof

Step Hyp Ref Expression
1 pnpncand.1
 |-  ( ph -> A e. CC )
2 pnpncand.2
 |-  ( ph -> B e. CC )
3 pnpncand.3
 |-  ( ph -> C e. CC )
4 2 3 subcld
 |-  ( ph -> ( B - C ) e. CC )
5 1 4 addcld
 |-  ( ph -> ( A + ( B - C ) ) e. CC )
6 5 2 3 subsub2d
 |-  ( ph -> ( ( A + ( B - C ) ) - ( B - C ) ) = ( ( A + ( B - C ) ) + ( C - B ) ) )
7 1 4 pncand
 |-  ( ph -> ( ( A + ( B - C ) ) - ( B - C ) ) = A )
8 6 7 eqtr3d
 |-  ( ph -> ( ( A + ( B - C ) ) + ( C - B ) ) = A )