Description: Introducing subtraction on both sides of a statement of inequality. Contrapositive of subcan2d . (Contributed by David Moews, 28Feb2017)
Ref  Expression  

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

pncand.2   ( ph > B e. CC ) 

subaddd.3   ( ph > C e. CC ) 

subneintr2d.4   ( ph > A =/= B ) 

Assertion  subneintr2d   ( ph > ( A  C ) =/= ( B  C ) ) 
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  subneintr2d.4   ( ph > A =/= B ) 

5  1 2 3  subcan2ad   ( ph > ( ( A  C ) = ( B  C ) <> A = B ) ) 
6  5  necon3bid   ( ph > ( ( A  C ) =/= ( B  C ) <> A =/= B ) ) 
7  4 6  mpbird   ( ph > ( A  C ) =/= ( B  C ) ) 