Description: A modus tollens deduction for inequality. (Contributed by Steven Nguyen, 1Jun2023)
Ref  Expression  

Hypotheses  mteqand.1   ( ph > C =/= D ) 

mteqand.2   ( ( ph /\ A = B ) > C = D ) 

Assertion  mteqand   ( ph > A =/= B ) 
Step  Hyp  Ref  Expression 

1  mteqand.1   ( ph > C =/= D ) 

2  mteqand.2   ( ( ph /\ A = B ) > C = D ) 

3  1  neneqd   ( ph > . C = D ) 
4  3 2  mtand   ( ph > . A = B ) 
5  4  neqned   ( ph > A =/= B ) 