Theorem necomi 3011

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

This proof depends on syntax axioms:   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ne 2958

This theorem is used by:  nesymi  3014  nesymir  3015  0nep0  5326  opthhausdorff  5498  xp01disj  8482  xp01disjl  8483  enpr2d  9059  snnen2o  9219  rex2dom  9227  djuexb  9918  djuin  9927  pnfnemnf  11292  mnfnepnf  11293  ltneii  11351  0ne1  12340  0ne2  12478  xnn0n0n1ge2b  13187  xmulpnf1  13330  fzprval  13644  fvf1tp  13854  hashneq0  14432  f1oun2prg  14992  geo2sum2  15967  ressplusg  17382  ressmulr  17398  fnpr2o  17649  fvpr0o  17651  fvpr1o  17652  rescabs  17928  odubas  18385  degenmgmnfn  19055  degenmgm  19056  degenmgm2  19059  symgvalstruct  19530  dmdprdpr  20184  dprdpr  20185  mgpress  20289  rmodislmod  21120  sralem  21366  srasca  21370  sratset  21373  srads  21375  cnfldfun  21605  cnfldfunALT  21606  zlmbas  21736  zlmplusg  21737  zlmmulr  21738  zlmsca  21739  znbas2  21758  znadd  21759  znmul  21760  opsrbas  22272  opsrplusg  22273  opsrmulr  22274  opsrvsca  22275  opsrsca  22276  xpstopnlem1  24041  tuslem  24498  setsmsbas  24707  tngbas  24873  tngplusg  24874  tngmulr  24876  tngsca  24877  tngvsca  24878  tngip  24879  2logb9irrALT  27043  sqrt2cxp2logb9e3  27044  1sgm2ppw  27444  2sqlem11  27673  nogesgn1ores  27918  nosepnelem  27923  noinfbnd1lem3  27969  noinfbnd1lem5  27971  noinfbnd2lem1  27974  ttgval  29339  ttgbas  29341  ttgplusg  29342  ttgvsca  29344  ttgds  29345  cchhllem  29351  axlowdimlem13  29419  usgrexmpldifpr  29726  usgrexmplef  29727  vdegp1ai  30004  vdegp1bi  30005  konigsbergiedgw  30736  konigsberglem2  30741  konigsberglem3  30742  ex-pss  30916  ex-hash  30941  resvbas  33782  resvplusg  33783  resvmulr  33785  2sqr3minply  34298  signswch  35077  bj-disjsn01  37704  bj-1upln0  37761  finxpreclem3  38155  hlhilsbase  42820  hlhilsplus  42821  hlhilsmul  42822  aks6d1c7lem1  43054  ine1  43197  remul01  43290  sn-0tie0  43347  flt0  43491  mnuprdlem2  45105  ovnsubadd2lem  47481  usgrexmpl1lem  48945  usgrexmpl2lem  48950  usgrexmpl2nb2  48957  gpgprismgr4cycllem7  49025  nnlog2ge0lt1  49504  logbpw2m1  49505  fllog2  49506  blennnelnn  49514  nnpw2blen  49518  blen1  49522  blen2  49523  blen1b  49526  blennnt2  49527  nnolog2flm1  49528  blennngt2o2  49530  blennn0e2  49532  inlinecirc02plem  49724  veronesev2lem  50815  veronesev3lem  50816  veronesevrowd  50820