Description: Contrapositive law deduction for inequality. (Contributed by NM, 29Jun2007)
Ref  Expression  

Hypothesis  necon4bid.1   ( ph > ( A =/= B <> C =/= D ) ) 

Assertion  necon4bid   ( ph > ( A = B <> C = D ) ) 
Step  Hyp  Ref  Expression 

1  necon4bid.1   ( ph > ( A =/= B <> C =/= D ) ) 

2  1  necon2bbid   ( ph > ( C = D <> . A =/= B ) ) 
3  nne   ( . A =/= B <> A = B ) 

4  2 3  syl6rbb   ( ph > ( A = B <> C = D ) ) 