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

Theorem necomi 2528
Description: Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
Hypothesis
Ref Expression
necomi.1  |-  A  =/= 
B
Assertion
Ref Expression
necomi  |-  B  =/= 
A

Proof of Theorem necomi
StepHypRef Expression
1 necomi.1 . 2  |-  A  =/= 
B
2 necom 2527 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2mpbi 199 1  |-  B  =/= 
A
Colors of variables: wff set class
Syntax hints:    =/= wne 2446
This theorem is referenced by:  0nep0  4181  xp01disj  6495  1sdom  7065  ltneii  8931  recgt0ii  9662  pnfnemnf  10459  xrnepnf  10461  xrltnr  10462  nltmnf  10468  xnegmnf  10537  xaddmnf1  10555  xaddmnf2  10556  mnfaddpnf  10558  xaddnepnf  10562  xmullem2  10585  xmulpnf1  10594  xadddilem  10614  fzprval  10844  resup  10971  geo2sum2  12330  prmreclem2  12964  xpscfn  13461  xpsc0  13462  xpsc1  13463  rescabs  13710  setcepi  13920  dmdprdpr  15284  dprdpr  15285  mgpress  15336  xpstopnlem1  17500  i1f1lem  19044  vieta1lem2  19691  mcubic  20143  cubic2  20144  asinlem  20164  sqff1o  20420  1sgm2ppw  20439  dchrpt  20506  lgsqr  20585  2sqlem11  20614  ex-pss  20815  indf1o  23607  konigsberg  23911  axlowdimlem13  24582  ftp  26893  bezoutr1  27073  wepwsolem  27138  mncn0  27344  aaitgo  27367  refsum2cnlem1  27708  f1oun2prg  28076  elprchashprn2  28088  s2f1o  28091  usgraedgprv  28122  usgra1v  28126  usgraexmpldifpr  28132  usgraexmpl  28133
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-ne 2448
  Copyright terms: Public domain W3C validator