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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  nesymi  2989  nesymir  2990  0nep0  5303  opthhausdorff  5465  xp01disj  8418  xp01disjl  8419  enpr2d  8985  snnen2o  9145  rex2dom  9153  djuexb  9821  djuin  9830  pnfnemnf  11187  mnfnepnf  11188  ltneii  11246  0ne1  12216  0ne2  12347  xnn0n0n1ge2b  13046  xmulpnf1  13189  fzprval  13501  fvf1tp  13709  hashneq0  14287  f1oun2prg  14840  geo2sum2  15797  ressplusg  17211  ressmulr  17227  fnpr2o  17478  fvpr0o  17480  fvpr1o  17481  rescabs  17757  odubas  18214  symgvalstruct  19326  dmdprdpr  19980  dprdpr  19981  mgpress  20085  rmodislmod  20881  sralem  21128  srasca  21132  sratset  21135  srads  21137  cnfldfun  21323  cnfldfunALT  21324  cnfldfunOLD  21336  cnfldfunALTOLD  21337  zlmbas  21472  zlmplusg  21473  zlmmulr  21474  zlmsca  21475  znbas2  21494  znadd  21495  znmul  21496  opsrbas  22005  opsrplusg  22006  opsrmulr  22007  opsrvsca  22008  opsrsca  22009  xpstopnlem1  23753  tuslem  24210  setsmsbas  24419  tngbas  24585  tngplusg  24586  tngmulr  24588  tngsca  24589  tngvsca  24590  tngip  24591  2logb9irrALT  26764  sqrt2cxp2logb9e3  26765  1sgm2ppw  27167  2sqlem11  27396  nogesgn1ores  27642  nosepnelem  27647  noinfbnd1lem3  27693  noinfbnd1lem5  27695  noinfbnd2lem1  27698  ttgval  28947  ttgbas  28949  ttgplusg  28950  ttgvsca  28952  ttgds  28953  cchhllem  28959  axlowdimlem13  29027  usgrexmpldifpr  29331  usgrexmplef  29332  vdegp1ai  29610  vdegp1bi  29611  konigsbergiedgw  30323  konigsberglem2  30328  konigsberglem3  30329  ex-pss  30503  ex-hash  30528  resvbas  33415  resvplusg  33416  resvmulr  33418  2sqr3minply  33937  signswch  34718  bj-disjsn01  37153  bj-1upln0  37210  finxpreclem3  37594  hlhilsbase  42195  hlhilsplus  42196  hlhilsmul  42197  aks6d1c7lem1  42430  ine1  42565  remul01  42658  sn-0tie0  42702  flt0  42876  mnuprdlem2  44510  ovnsubadd2lem  46885  nthrucw  47126  usgrexmpl1lem  48263  usgrexmpl2lem  48268  usgrexmpl2nb2  48275  gpgprismgr4cycllem7  48343  nnlog2ge0lt1  48808  logbpw2m1  48809  fllog2  48810  blennnelnn  48818  nnpw2blen  48822  blen1  48826  blen2  48827  blen1b  48830  blennnt2  48831  nnolog2flm1  48832  blennngt2o2  48834  blennn0e2  48836  inlinecirc02plem  49028