Theorem necomi 3010

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

Syntax hints:   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957

This theorem is referenced by:  nesymi  3013  nesymir  3014  0nep0  5313  opthhausdorff  5485  xp01disj  8455  xp01disjl  8456  enpr2d  9025  snnen2o  9185  rex2dom  9193  djuexb  9864  djuin  9873  pnfnemnf  11234  mnfnepnf  11235  ltneii  11293  0ne1  12286  0ne2  12424  xnn0n0n1ge2b  13131  xmulpnf1  13274  fzprval  13587  fvf1tp  13796  hashneq0  14374  f1oun2prg  14927  geo2sum2  15887  ressplusg  17303  ressmulr  17319  fnpr2o  17570  fvpr0o  17572  fvpr1o  17573  rescabs  17849  odubas  18306  symgvalstruct  19420  dmdprdpr  20074  dprdpr  20075  mgpress  20179  rmodislmod  20977  sralem  21223  srasca  21227  sratset  21230  srads  21232  cnfldfun  21418  cnfldfunALT  21419  zlmbas  21549  zlmplusg  21550  zlmmulr  21551  zlmsca  21552  znbas2  21571  znadd  21572  znmul  21573  opsrbas  22083  opsrplusg  22084  opsrmulr  22085  opsrvsca  22086  opsrsca  22087  xpstopnlem1  23849  tuslem  24306  setsmsbas  24515  tngbas  24681  tngplusg  24682  tngmulr  24684  tngsca  24685  tngvsca  24686  tngip  24687  2logb9irrALT  26840  sqrt2cxp2logb9e3  26841  1sgm2ppw  27241  2sqlem11  27470  nogesgn1ores  27715  nosepnelem  27720  noinfbnd1lem3  27766  noinfbnd1lem5  27768  noinfbnd2lem1  27771  ttgval  29021  ttgbas  29023  ttgplusg  29024  ttgvsca  29026  ttgds  29027  cchhllem  29033  axlowdimlem13  29101  usgrexmpldifpr  29405  usgrexmplef  29406  vdegp1ai  29683  vdegp1bi  29684  konigsbergiedgw  30396  konigsberglem2  30401  konigsberglem3  30402  ex-pss  30576  ex-hash  30601  resvbas  33481  resvplusg  33482  resvmulr  33484  2sqr3minply  34038  signswch  34819  bj-disjsn01  37401  bj-1upln0  37458  finxpreclem3  37851  hlhilsbase  42527  hlhilsplus  42528  hlhilsmul  42529  aks6d1c7lem1  42761  ine1  42887  remul01  42980  sn-0tie0  43037  flt0  43183  mnuprdlem2  44813  ovnsubadd2lem  47183  nthrucw  47426  usgrexmpl1lem  48607  usgrexmpl2lem  48612  usgrexmpl2nb2  48619  gpgprismgr4cycllem7  48687  nnlog2ge0lt1  49152  logbpw2m1  49153  fllog2  49154  blennnelnn  49162  nnpw2blen  49166  blen1  49170  blen2  49171  blen1b  49174  blennnt2  49175  nnolog2flm1  49176  blennngt2o2  49178  blennn0e2  49180  inlinecirc02plem  49372