Description: Deduction from equality to inequality. (Contributed by NM, 23Feb2005) (Proof shortened by Andrew Salmon, 25May2011)
Ref  Expression  

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

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

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

2  dfne   ( A =/= B <> . A = B ) 

3  1  necon3bbid   ( ph > ( . A = B <> C =/= D ) ) 
4  2 3  syl5bb   ( ph > ( A =/= B <> C =/= D ) ) 