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

Hypotheses  neeq1d.1   ( ph > A = B ) 

neeq12d.2   ( ph > C = D ) 

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

1  neeq1d.1   ( ph > A = B ) 

2  neeq12d.2   ( ph > C = D ) 

3  1 2  eqeq12d   ( ph > ( A = C <> B = D ) ) 
4  3  necon3bid   ( ph > ( A =/= C <> B =/= D ) ) 