Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  necomi Unicode version

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
StepHypRef Expression
1 necomi.1 . 2
2 necom 2726 . 2
31, 2mpbi 208 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator