Description: Deduction from commutative law for inequality. (Contributed by NM, 12Feb2008)
Ref  Expression  

Hypothesis  necomd.1   ( ph > A =/= B ) 

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

1  necomd.1   ( ph > A =/= B ) 

2  necom   ( A =/= B <> B =/= A ) 

3  1 2  sylib   ( ph > B =/= A ) 