Theorem necomi 2986

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

Syntax hints:   ≠ wne 2932

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  nesymi  2989  nesymir  2990  0nep0  5328  opthhausdorff  5492  xp01disj  8501  xp01disjl  8502  enpr2d  9061  snnen2o  9243  rex2dom  9252  1sdomOLD  9255  djuexb  9921  djuin  9930  pnfnemnf  11288  mnfnepnf  11289  ltneii  11346  0ne1  12309  0ne2  12445  xnn0n0n1ge2b  13146  xmulpnf1  13288  fzprval  13600  fvf1tp  13804  hashneq0  14380  f1oun2prg  14934  geo2sum2  15888  ressplusg  17303  ressmulr  17319  fnpr2o  17569  fvpr0o  17571  fvpr1o  17572  rescabs  17844  odubas  18301  symgvalstruct  19376  dmdprdpr  20030  dprdpr  20031  mgpress  20108  rmodislmod  20885  sralem  21132  srasca  21136  sratset  21139  srads  21141  cnfldfun  21327  cnfldfunALT  21328  cnfldfunOLD  21340  cnfldfunALTOLD  21341  zlmbas  21476  zlmplusg  21477  zlmmulr  21478  zlmsca  21479  znbas2  21498  znadd  21499  znmul  21500  opsrbas  22006  opsrplusg  22007  opsrmulr  22008  opsrvsca  22009  opsrsca  22010  xpstopnlem1  23745  tuslem  24203  setsmsbas  24412  tngbas  24578  tngplusg  24579  tngmulr  24581  tngsca  24582  tngvsca  24583  tngip  24584  2logb9irrALT  26758  sqrt2cxp2logb9e3  26759  1sgm2ppw  27161  2sqlem11  27390  nogesgn1ores  27636  nosepnelem  27641  noinfbnd1lem3  27687  noinfbnd1lem5  27689  noinfbnd2lem1  27692  ttgval  28800  ttgbas  28802  ttgplusg  28803  ttgvsca  28805  ttgds  28806  cchhllem  28812  axlowdimlem13  28879  usgrexmpldifpr  29183  usgrexmplef  29184  vdegp1ai  29462  vdegp1bi  29463  konigsbergiedgw  30175  konigsberglem2  30180  konigsberglem3  30181  ex-pss  30355  ex-hash  30380  resvbas  33296  resvplusg  33297  resvmulr  33299  2sqr3minply  33760  signswch  34539  bj-disjsn01  36916  bj-1upln0  36973  finxpreclem3  37357  hlhilsbase  41904  hlhilsplus  41905  hlhilsmul  41906  aks6d1c7lem1  42139  ine1  42310  remul01  42397  sn-0tie0  42429  flt0  42607  mnuprdlem2  44245  ovnsubadd2lem  46622  usgrexmpl1lem  47973  usgrexmpl2lem  47978  usgrexmpl2nb2  47985  gpgprismgr4cycllem7  48048  nnlog2ge0lt1  48494  logbpw2m1  48495  fllog2  48496  blennnelnn  48504  nnpw2blen  48508  blen1  48512  blen2  48513  blen1b  48516  blennnt2  48517  nnolog2flm1  48518  blennngt2o2  48520  blennn0e2  48522  inlinecirc02plem  48714