Theorem necomi 2989

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 2988	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
3	1, 2	mpbi 231	1 ⊢ 𝐵 ≠ 𝐴

Syntax hints:   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ne 2936

This theorem is referenced by:  nesymi  2992  nesymir  2993  0nep0  5293  opthhausdorff  5465  xp01disj  8423  xp01disjl  8424  enpr2d  8992  snnen2o  9152  rex2dom  9160  djuexb  9831  djuin  9840  pnfnemnf  11198  mnfnepnf  11199  ltneii  11257  0ne1  12250  0ne2  12381  xnn0n0n1ge2b  13081  xmulpnf1  13224  fzprval  13537  fvf1tp  13746  hashneq0  14324  f1oun2prg  14877  geo2sum2  15837  ressplusg  17252  ressmulr  17268  fnpr2o  17519  fvpr0o  17521  fvpr1o  17522  rescabs  17798  odubas  18255  symgvalstruct  19370  dmdprdpr  20024  dprdpr  20025  mgpress  20129  rmodislmod  20927  sralem  21173  srasca  21177  sratset  21180  srads  21182  cnfldfun  21368  cnfldfunALT  21369  zlmbas  21499  zlmplusg  21500  zlmmulr  21501  zlmsca  21502  znbas2  21521  znadd  21522  znmul  21523  opsrbas  22033  opsrplusg  22034  opsrmulr  22035  opsrvsca  22036  opsrsca  22037  xpstopnlem1  23799  tuslem  24256  setsmsbas  24465  tngbas  24631  tngplusg  24632  tngmulr  24634  tngsca  24635  tngvsca  24636  tngip  24637  2logb9irrALT  26787  sqrt2cxp2logb9e3  26788  1sgm2ppw  27188  2sqlem11  27417  nogesgn1ores  27663  nosepnelem  27668  noinfbnd1lem3  27714  noinfbnd1lem5  27716  noinfbnd2lem1  27719  ttgval  28968  ttgbas  28970  ttgplusg  28971  ttgvsca  28973  ttgds  28974  cchhllem  28980  axlowdimlem13  29048  usgrexmpldifpr  29352  usgrexmplef  29353  vdegp1ai  29630  vdegp1bi  29631  konigsbergiedgw  30343  konigsberglem2  30348  konigsberglem3  30349  ex-pss  30523  ex-hash  30548  resvbas  33424  resvplusg  33425  resvmulr  33427  2sqr3minply  33971  signswch  34752  bj-disjsn01  37312  bj-1upln0  37369  finxpreclem3  37762  hlhilsbase  42438  hlhilsplus  42439  hlhilsmul  42440  aks6d1c7lem1  42672  ine1  42798  remul01  42891  sn-0tie0  42948  flt0  43094  mnuprdlem2  44724  ovnsubadd2lem  47095  nthrucw  47338  usgrexmpl1lem  48519  usgrexmpl2lem  48524  usgrexmpl2nb2  48531  gpgprismgr4cycllem7  48599  nnlog2ge0lt1  49064  logbpw2m1  49065  fllog2  49066  blennnelnn  49074  nnpw2blen  49078  blen1  49082  blen2  49083  blen1b  49086  blennnt2  49087  nnolog2flm1  49088  blennngt2o2  49090  blennn0e2  49092  inlinecirc02plem  49284