Theorem necomi 2992

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

Syntax hints:   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ne 2938

This theorem is referenced by:  nesymi  2995  nesymir  2996  0nep0  5363  opthhausdorff  5526  xp01disj  8527  xp01disjl  8528  enpr2d  9087  snnen2o  9270  rex2dom  9279  1sdomOLD  9282  djuexb  9946  djuin  9955  pnfnemnf  11313  mnfnepnf  11314  ltneii  11371  0ne1  12334  0ne2  12470  xnn0n0n1ge2b  13170  xmulpnf1  13312  fzprval  13621  fvf1tp  13825  hashneq0  14399  f1oun2prg  14952  geo2sum2  15906  ressplusg  17335  ressmulr  17352  fnpr2o  17603  fvpr0o  17605  fvpr1o  17606  rescabs  17882  rescabsOLD  17883  odubas  18347  symgvalstruct  19428  symgvalstructOLD  19429  dmdprdpr  20083  dprdpr  20084  mgpress  20166  mgpressOLD  20167  rmodislmod  20944  sralem  21192  srasca  21200  sratset  21205  srads  21208  cnfldfun  21395  cnfldfunALT  21396  cnfldfunOLD  21408  cnfldfunALTOLD  21409  zlmbas  21546  zlmplusg  21548  zlmmulr  21550  zlmsca  21552  znbas2  21572  znadd  21574  znmul  21576  opsrbas  22086  opsrplusg  22088  opsrmulr  22090  opsrvsca  22092  opsrsca  22094  xpstopnlem1  23832  tuslem  24290  setsmsbas  24500  tngbas  24670  tngplusg  24672  tngmulr  24675  tngsca  24677  tngvsca  24679  tngip  24681  2logb9irrALT  26855  sqrt2cxp2logb9e3  26856  1sgm2ppw  27258  2sqlem11  27487  nogesgn1ores  27733  nosepnelem  27738  noinfbnd1lem3  27784  noinfbnd1lem5  27786  noinfbnd2lem1  27789  ttgval  28897  ttgbas  28901  ttgplusg  28903  ttgvsca  28906  ttgds  28908  cchhllem  28915  axlowdimlem13  28983  usgrexmpldifpr  29289  usgrexmplef  29290  vdegp1ai  29568  vdegp1bi  29569  konigsbergiedgw  30276  konigsberglem2  30281  konigsberglem3  30282  ex-pss  30456  ex-hash  30481  resvbas  33338  resvplusg  33340  resvmulr  33344  2sqr3minply  33752  signswch  34554  bj-disjsn01  36934  bj-1upln0  36991  finxpreclem3  37375  hlhilsbase  41922  hlhilsplus  41924  hlhilsmul  41926  aks6d1c7lem1  42161  ine1  42327  remul01  42413  sn-0tie0  42445  flt0  42623  mnuprdlem2  44268  ovnsubadd2lem  46600  usgrexmpl1lem  47915  usgrexmpl2lem  47920  usgrexmpl2nb2  47927  nnlog2ge0lt1  48415  logbpw2m1  48416  fllog2  48417  blennnelnn  48425  nnpw2blen  48429  blen1  48433  blen2  48434  blen1b  48437  blennnt2  48438  nnolog2flm1  48439  blennngt2o2  48441  blennn0e2  48443  inlinecirc02plem  48635