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 ) |
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 ) |