Theorem necomi 2980

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

Syntax hints:   ≠ wne 2926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ne 2927

This theorem is referenced by:  nesymi  2983  nesymir  2984  0nep0  5316  opthhausdorff  5480  xp01disj  8458  xp01disjl  8459  enpr2d  9023  snnen2o  9191  rex2dom  9200  1sdomOLD  9203  djuexb  9869  djuin  9878  pnfnemnf  11236  mnfnepnf  11237  ltneii  11294  0ne1  12264  0ne2  12395  xnn0n0n1ge2b  13099  xmulpnf1  13241  fzprval  13553  fvf1tp  13758  hashneq0  14336  f1oun2prg  14890  geo2sum2  15847  ressplusg  17261  ressmulr  17277  fnpr2o  17527  fvpr0o  17529  fvpr1o  17530  rescabs  17802  odubas  18259  symgvalstruct  19334  dmdprdpr  19988  dprdpr  19989  mgpress  20066  rmodislmod  20843  sralem  21090  srasca  21094  sratset  21097  srads  21099  cnfldfun  21285  cnfldfunALT  21286  cnfldfunOLD  21298  cnfldfunALTOLD  21299  zlmbas  21434  zlmplusg  21435  zlmmulr  21436  zlmsca  21437  znbas2  21456  znadd  21457  znmul  21458  opsrbas  21964  opsrplusg  21965  opsrmulr  21966  opsrvsca  21967  opsrsca  21968  xpstopnlem1  23703  tuslem  24161  setsmsbas  24370  tngbas  24536  tngplusg  24537  tngmulr  24539  tngsca  24540  tngvsca  24541  tngip  24542  2logb9irrALT  26715  sqrt2cxp2logb9e3  26716  1sgm2ppw  27118  2sqlem11  27347  nogesgn1ores  27593  nosepnelem  27598  noinfbnd1lem3  27644  noinfbnd1lem5  27646  noinfbnd2lem1  27649  ttgval  28809  ttgbas  28811  ttgplusg  28812  ttgvsca  28814  ttgds  28815  cchhllem  28821  axlowdimlem13  28888  usgrexmpldifpr  29192  usgrexmplef  29193  vdegp1ai  29471  vdegp1bi  29472  konigsbergiedgw  30184  konigsberglem2  30189  konigsberglem3  30190  ex-pss  30364  ex-hash  30389  resvbas  33313  resvplusg  33314  resvmulr  33316  2sqr3minply  33777  signswch  34559  bj-disjsn01  36947  bj-1upln0  37004  finxpreclem3  37388  hlhilsbase  41940  hlhilsplus  41941  hlhilsmul  41942  aks6d1c7lem1  42175  ine1  42309  remul01  42402  sn-0tie0  42446  flt0  42632  mnuprdlem2  44269  ovnsubadd2lem  46650  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2nb2  48028  gpgprismgr4cycllem7  48095  nnlog2ge0lt1  48559  logbpw2m1  48560  fllog2  48561  blennnelnn  48569  nnpw2blen  48573  blen1  48577  blen2  48578  blen1b  48581  blennnt2  48582  nnolog2flm1  48583  blennngt2o2  48585  blennn0e2  48587  inlinecirc02plem  48779