Description: Cancellation law for subtraction. (Contributed by Mario Carneiro, 27May2016)
Ref  Expression  

Hypotheses  negidd.1   ( ph > A e. CC ) 

pncand.2   ( ph > B e. CC ) 

subaddd.3   ( ph > C e. CC ) 

Assertion  nnncan2d   ( ph > ( ( A  C )  ( B  C ) ) = ( A  B ) ) 
Step  Hyp  Ref  Expression 

1  negidd.1   ( ph > A e. CC ) 

2  pncand.2   ( ph > B e. CC ) 

3  subaddd.3   ( ph > C e. CC ) 

4  nnncan2   ( ( A e. CC /\ B e. CC /\ C e. CC ) > ( ( A  C )  ( B  C ) ) = ( A  B ) ) 

5  1 2 3 4  syl3anc   ( ph > ( ( A  C )  ( B  C ) ) = ( A  B ) ) 