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 229	1 ⊢ 𝐵 ≠ 𝐴

Syntax hints:   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716  df-ne 2933

This theorem is referenced by:  nesymi  2990  nesymir  2991  0nep0  5346  opthhausdorff  5507  xp01disj  8486  xp01disjl  8487  enpr2d  9045  snnen2o  9233  rex2dom  9242  1sdomOLD  9245  djuexb  9900  djuin  9909  pnfnemnf  11266  mnfnepnf  11267  ltneii  11324  0ne1  12280  0ne2  12416  xnn0n0n1ge2b  13108  xmulpnf1  13250  fzprval  13559  hashneq0  14321  f1oun2prg  14865  geo2sum2  15817  ressplusg  17234  ressmulr  17251  fnpr2o  17502  fvpr0o  17504  fvpr1o  17505  rescabs  17781  rescabsOLD  17782  odubas  18246  symgvalstruct  19306  symgvalstructOLD  19307  dmdprdpr  19961  dprdpr  19962  mgpress  20044  mgpressOLD  20045  rmodislmod  20766  sralem  21014  srasca  21022  sratset  21027  srads  21030  cnfldfun  21240  cnfldfunALT  21241  zlmbas  21373  zlmplusg  21375  zlmmulr  21377  zlmsca  21379  znbas2  21399  znadd  21401  znmul  21403  opsrbas  21916  opsrplusg  21918  opsrmulr  21920  opsrvsca  21922  opsrsca  21924  xpstopnlem1  23635  tuslem  24093  setsmsbas  24303  tngbas  24473  tngplusg  24475  tngmulr  24478  tngsca  24480  tngvsca  24482  tngip  24484  2logb9irrALT  26646  sqrt2cxp2logb9e3  26647  1sgm2ppw  27049  2sqlem11  27278  nogesgn1ores  27523  nosepnelem  27528  noinfbnd1lem3  27574  noinfbnd1lem5  27576  noinfbnd2lem1  27579  ttgval  28595  ttgbas  28599  ttgplusg  28601  ttgvsca  28604  ttgds  28606  cchhllem  28613  axlowdimlem13  28681  usgrexmpldifpr  28984  usgrexmplef  28985  vdegp1ai  29262  vdegp1bi  29263  konigsbergiedgw  29970  konigsberglem2  29975  konigsberglem3  29976  ex-pss  30150  ex-hash  30175  resvbas  32913  resvplusg  32915  resvmulr  32919  signswch  34061  gg-cnfldfun  35670  gg-cnfldfunALT  35671  bj-disjsn01  36323  bj-1upln0  36380  finxpreclem3  36764  hlhilsbase  41301  hlhilsplus  41303  hlhilsmul  41305  remul01  41769  sn-0tie0  41801  flt0  41868  mnuprdlem2  43521  ovnsubadd2lem  45846  nnlog2ge0lt1  47440  logbpw2m1  47441  fllog2  47442  blennnelnn  47450  nnpw2blen  47454  blen1  47458  blen2  47459  blen1b  47462  blennnt2  47463  nnolog2flm1  47464  blennngt2o2  47466  blennn0e2  47468  inlinecirc02plem  47660