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  5300  opthhausdorff  5464  xp01disj  8416  xp01disjl  8417  enpr2d  8981  snnen2o  9144  rex2dom  9152  djuexb  9824  djuin  9833  pnfnemnf  11189  mnfnepnf  11190  ltneii  11247  0ne1  12217  0ne2  12348  xnn0n0n1ge2b  13052  xmulpnf1  13194  fzprval  13506  fvf1tp  13711  hashneq0  14289  f1oun2prg  14842  geo2sum2  15799  ressplusg  17213  ressmulr  17229  fnpr2o  17479  fvpr0o  17481  fvpr1o  17482  rescabs  17758  odubas  18215  symgvalstruct  19294  dmdprdpr  19948  dprdpr  19949  mgpress  20053  rmodislmod  20851  sralem  21098  srasca  21102  sratset  21105  srads  21107  cnfldfun  21293  cnfldfunALT  21294  cnfldfunOLD  21306  cnfldfunALTOLD  21307  zlmbas  21442  zlmplusg  21443  zlmmulr  21444  zlmsca  21445  znbas2  21464  znadd  21465  znmul  21466  opsrbas  21973  opsrplusg  21974  opsrmulr  21975  opsrvsca  21976  opsrsca  21977  xpstopnlem1  23712  tuslem  24170  setsmsbas  24379  tngbas  24545  tngplusg  24546  tngmulr  24548  tngsca  24549  tngvsca  24550  tngip  24551  2logb9irrALT  26724  sqrt2cxp2logb9e3  26725  1sgm2ppw  27127  2sqlem11  27356  nogesgn1ores  27602  nosepnelem  27607  noinfbnd1lem3  27653  noinfbnd1lem5  27655  noinfbnd2lem1  27658  ttgval  28838  ttgbas  28840  ttgplusg  28841  ttgvsca  28843  ttgds  28844  cchhllem  28850  axlowdimlem13  28917  usgrexmpldifpr  29221  usgrexmplef  29222  vdegp1ai  29500  vdegp1bi  29501  konigsbergiedgw  30210  konigsberglem2  30215  konigsberglem3  30216  ex-pss  30390  ex-hash  30415  resvbas  33282  resvplusg  33283  resvmulr  33285  2sqr3minply  33746  signswch  34528  bj-disjsn01  36925  bj-1upln0  36982  finxpreclem3  37366  hlhilsbase  41918  hlhilsplus  41919  hlhilsmul  41920  aks6d1c7lem1  42153  ine1  42287  remul01  42380  sn-0tie0  42424  flt0  42610  mnuprdlem2  44246  ovnsubadd2lem  46627  usgrexmpl1lem  48006  usgrexmpl2lem  48011  usgrexmpl2nb2  48018  gpgprismgr4cycllem7  48086  nnlog2ge0lt1  48552  logbpw2m1  48553  fllog2  48554  blennnelnn  48562  nnpw2blen  48566  blen1  48570  blen2  48571  blen1b  48574  blennnt2  48575  nnolog2flm1  48576  blennngt2o2  48578  blennn0e2  48580  inlinecirc02plem  48772