Theorem necomi 2987

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

Syntax hints:   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  nesymi  2990  nesymir  2991  0nep0  5295  opthhausdorff  5465  xp01disj  8419  xp01disjl  8420  enpr2d  8988  snnen2o  9148  rex2dom  9156  djuexb  9824  djuin  9833  pnfnemnf  11191  mnfnepnf  11192  ltneii  11250  0ne1  12243  0ne2  12374  xnn0n0n1ge2b  13074  xmulpnf1  13217  fzprval  13530  fvf1tp  13739  hashneq0  14317  f1oun2prg  14870  geo2sum2  15830  ressplusg  17245  ressmulr  17261  fnpr2o  17512  fvpr0o  17514  fvpr1o  17515  rescabs  17791  odubas  18248  symgvalstruct  19363  dmdprdpr  20017  dprdpr  20018  mgpress  20122  rmodislmod  20916  sralem  21163  srasca  21167  sratset  21170  srads  21172  cnfldfun  21358  cnfldfunALT  21359  cnfldfunOLD  21371  cnfldfunALTOLD  21372  zlmbas  21507  zlmplusg  21508  zlmmulr  21509  zlmsca  21510  znbas2  21529  znadd  21530  znmul  21531  opsrbas  22038  opsrplusg  22039  opsrmulr  22040  opsrvsca  22041  opsrsca  22042  xpstopnlem1  23784  tuslem  24241  setsmsbas  24450  tngbas  24616  tngplusg  24617  tngmulr  24619  tngsca  24620  tngvsca  24621  tngip  24622  2logb9irrALT  26775  sqrt2cxp2logb9e3  26776  1sgm2ppw  27177  2sqlem11  27406  nogesgn1ores  27652  nosepnelem  27657  noinfbnd1lem3  27703  noinfbnd1lem5  27705  noinfbnd2lem1  27708  ttgval  28957  ttgbas  28959  ttgplusg  28960  ttgvsca  28962  ttgds  28963  cchhllem  28969  axlowdimlem13  29037  usgrexmpldifpr  29341  usgrexmplef  29342  vdegp1ai  29620  vdegp1bi  29621  konigsbergiedgw  30333  konigsberglem2  30338  konigsberglem3  30339  ex-pss  30513  ex-hash  30538  resvbas  33409  resvplusg  33410  resvmulr  33412  2sqr3minply  33940  signswch  34721  bj-disjsn01  37275  bj-1upln0  37332  finxpreclem3  37723  hlhilsbase  42399  hlhilsplus  42400  hlhilsmul  42401  aks6d1c7lem1  42633  ine1  42760  remul01  42853  sn-0tie0  42910  flt0  43084  mnuprdlem2  44718  ovnsubadd2lem  47091  nthrucw  47332  usgrexmpl1lem  48509  usgrexmpl2lem  48514  usgrexmpl2nb2  48521  gpgprismgr4cycllem7  48589  nnlog2ge0lt1  49054  logbpw2m1  49055  fllog2  49056  blennnelnn  49064  nnpw2blen  49068  blen1  49072  blen2  49073  blen1b  49076  blennnt2  49077  nnolog2flm1  49078  blennngt2o2  49080  blennn0e2  49082  inlinecirc02plem  49274