Theorem necomi 2979

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

Syntax hints:   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  nesymi  2982  nesymir  2983  0nep0  5313  opthhausdorff  5477  xp01disj  8455  xp01disjl  8456  enpr2d  9020  snnen2o  9184  rex2dom  9193  1sdomOLD  9196  djuexb  9862  djuin  9871  pnfnemnf  11229  mnfnepnf  11230  ltneii  11287  0ne1  12257  0ne2  12388  xnn0n0n1ge2b  13092  xmulpnf1  13234  fzprval  13546  fvf1tp  13751  hashneq0  14329  f1oun2prg  14883  geo2sum2  15840  ressplusg  17254  ressmulr  17270  fnpr2o  17520  fvpr0o  17522  fvpr1o  17523  rescabs  17795  odubas  18252  symgvalstruct  19327  dmdprdpr  19981  dprdpr  19982  mgpress  20059  rmodislmod  20836  sralem  21083  srasca  21087  sratset  21090  srads  21092  cnfldfun  21278  cnfldfunALT  21279  cnfldfunOLD  21291  cnfldfunALTOLD  21292  zlmbas  21427  zlmplusg  21428  zlmmulr  21429  zlmsca  21430  znbas2  21449  znadd  21450  znmul  21451  opsrbas  21957  opsrplusg  21958  opsrmulr  21959  opsrvsca  21960  opsrsca  21961  xpstopnlem1  23696  tuslem  24154  setsmsbas  24363  tngbas  24529  tngplusg  24530  tngmulr  24532  tngsca  24533  tngvsca  24534  tngip  24535  2logb9irrALT  26708  sqrt2cxp2logb9e3  26709  1sgm2ppw  27111  2sqlem11  27340  nogesgn1ores  27586  nosepnelem  27591  noinfbnd1lem3  27637  noinfbnd1lem5  27639  noinfbnd2lem1  27642  ttgval  28802  ttgbas  28804  ttgplusg  28805  ttgvsca  28807  ttgds  28808  cchhllem  28814  axlowdimlem13  28881  usgrexmpldifpr  29185  usgrexmplef  29186  vdegp1ai  29464  vdegp1bi  29465  konigsbergiedgw  30177  konigsberglem2  30182  konigsberglem3  30183  ex-pss  30357  ex-hash  30382  resvbas  33306  resvplusg  33307  resvmulr  33309  2sqr3minply  33770  signswch  34552  bj-disjsn01  36940  bj-1upln0  36997  finxpreclem3  37381  hlhilsbase  41933  hlhilsplus  41934  hlhilsmul  41935  aks6d1c7lem1  42168  ine1  42302  remul01  42395  sn-0tie0  42439  flt0  42625  mnuprdlem2  44262  ovnsubadd2lem  46643  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2nb2  48024  gpgprismgr4cycllem7  48091  nnlog2ge0lt1  48555  logbpw2m1  48556  fllog2  48557  blennnelnn  48565  nnpw2blen  48569  blen1  48573  blen2  48574  blen1b  48577  blennnt2  48578  nnolog2flm1  48579  blennngt2o2  48581  blennn0e2  48583  inlinecirc02plem  48775