Theorem necomi 2727

Description: Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)

Hypothesis

Ref	Expression
necomi.1

Assertion

Ref	Expression
necomi

Proof of Theorem necomi

Step	Hyp	Ref	Expression
1		necomi.1	. 2
2		necom 2726	. 2
3	1, 2	mpbi 208	1

Syntax hints:  =/=wne 2652

This theorem is referenced by:  nesymi  2730  nesymir  2732  0nep0  4623  xp01disj  7165  1sdom  7742  ltneii  9718  0ne1  10628  0ne2  10772  pnfnemnf  11355  mnfnepnf  11356  xmulpnf1  11495  fzprval  11769  hashneq0  12434  f1oun2prg  12865  geo2sum2  13683  xpscfn  14956  xpsc0  14957  xpsc1  14958  rescabs  15202  dmdprdpr  17098  dprdpr  17099  mgpress  17152  xpstopnlem1  20310  1sgm2ppw  23475  2sqlem11  23650  axlowdimlem13  24257  usgraexmpldifpr  24400  usgraexmpl  24401  constr3lem4  24647  ex-pss  25149  signswch  28518  fprodn0f  31594  bj-disjsn01  34506  bj-1upln0  34567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654