Description: Deduction for inequality. (Contributed by NM, 25Oct1999) (Proof shortened by Wolf Lammen, 19Nov2019)
Ref  Expression  

Hypothesis  neeq1d.1   ( ph > A = B ) 

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

1  neeq1d.1   ( ph > A = B ) 

2  1  eqeq1d   ( ph > ( A = C <> B = C ) ) 
3  2  necon3bid   ( ph > ( A =/= C <> B =/= C ) ) 