Theorem necomi 2983

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

Syntax hints:   ≠ wne 2929

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 2705

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

This theorem is referenced by:  nesymi  2986  nesymir  2987  0nep0  5298  opthhausdorff  5460  xp01disj  8412  xp01disjl  8413  enpr2d  8977  snnen2o  9136  rex2dom  9144  djuexb  9809  djuin  9818  pnfnemnf  11174  mnfnepnf  11175  ltneii  11233  0ne1  12203  0ne2  12334  xnn0n0n1ge2b  13033  xmulpnf1  13175  fzprval  13487  fvf1tp  13695  hashneq0  14273  f1oun2prg  14826  geo2sum2  15783  ressplusg  17197  ressmulr  17213  fnpr2o  17463  fvpr0o  17465  fvpr1o  17466  rescabs  17742  odubas  18199  symgvalstruct  19311  dmdprdpr  19965  dprdpr  19966  mgpress  20070  rmodislmod  20865  sralem  21112  srasca  21116  sratset  21119  srads  21121  cnfldfun  21307  cnfldfunALT  21308  cnfldfunOLD  21320  cnfldfunALTOLD  21321  zlmbas  21456  zlmplusg  21457  zlmmulr  21458  zlmsca  21459  znbas2  21478  znadd  21479  znmul  21480  opsrbas  21986  opsrplusg  21987  opsrmulr  21988  opsrvsca  21989  opsrsca  21990  xpstopnlem1  23725  tuslem  24182  setsmsbas  24391  tngbas  24557  tngplusg  24558  tngmulr  24560  tngsca  24561  tngvsca  24562  tngip  24563  2logb9irrALT  26736  sqrt2cxp2logb9e3  26737  1sgm2ppw  27139  2sqlem11  27368  nogesgn1ores  27614  nosepnelem  27619  noinfbnd1lem3  27665  noinfbnd1lem5  27667  noinfbnd2lem1  27670  ttgval  28854  ttgbas  28856  ttgplusg  28857  ttgvsca  28859  ttgds  28860  cchhllem  28866  axlowdimlem13  28934  usgrexmpldifpr  29238  usgrexmplef  29239  vdegp1ai  29517  vdegp1bi  29518  konigsbergiedgw  30230  konigsberglem2  30235  konigsberglem3  30236  ex-pss  30410  ex-hash  30435  resvbas  33306  resvplusg  33307  resvmulr  33309  2sqr3minply  33814  signswch  34595  bj-disjsn01  37017  bj-1upln0  37074  finxpreclem3  37458  hlhilsbase  42058  hlhilsplus  42059  hlhilsmul  42060  aks6d1c7lem1  42293  ine1  42432  remul01  42525  sn-0tie0  42569  flt0  42755  mnuprdlem2  44390  ovnsubadd2lem  46767  nthrucw  47008  usgrexmpl1lem  48145  usgrexmpl2lem  48150  usgrexmpl2nb2  48157  gpgprismgr4cycllem7  48225  nnlog2ge0lt1  48691  logbpw2m1  48692  fllog2  48693  blennnelnn  48701  nnpw2blen  48705  blen1  48709  blen2  48710  blen1b  48713  blennnt2  48714  nnolog2flm1  48715  blennngt2o2  48717  blennn0e2  48719  inlinecirc02plem  48911