Theorem necomi 2995

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

Syntax hints:   ≠ wne 2940

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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  nesymi  2998  nesymir  2999  0nep0  5358  opthhausdorff  5522  xp01disj  8529  xp01disjl  8530  enpr2d  9089  snnen2o  9273  rex2dom  9282  1sdomOLD  9285  djuexb  9949  djuin  9958  pnfnemnf  11316  mnfnepnf  11317  ltneii  11374  0ne1  12337  0ne2  12473  xnn0n0n1ge2b  13174  xmulpnf1  13316  fzprval  13625  fvf1tp  13829  hashneq0  14403  f1oun2prg  14956  geo2sum2  15910  ressplusg  17334  ressmulr  17351  fnpr2o  17602  fvpr0o  17604  fvpr1o  17605  rescabs  17877  rescabsOLD  17878  odubas  18336  symgvalstruct  19414  symgvalstructOLD  19415  dmdprdpr  20069  dprdpr  20070  mgpress  20147  rmodislmod  20928  sralem  21175  srasca  21183  sratset  21188  srads  21191  cnfldfun  21378  cnfldfunALT  21379  cnfldfunOLD  21391  cnfldfunALTOLD  21392  zlmbas  21529  zlmplusg  21531  zlmmulr  21533  zlmsca  21535  znbas2  21555  znadd  21557  znmul  21559  opsrbas  22069  opsrplusg  22071  opsrmulr  22073  opsrvsca  22075  opsrsca  22077  xpstopnlem1  23817  tuslem  24275  setsmsbas  24485  tngbas  24655  tngplusg  24657  tngmulr  24660  tngsca  24662  tngvsca  24664  tngip  24666  2logb9irrALT  26841  sqrt2cxp2logb9e3  26842  1sgm2ppw  27244  2sqlem11  27473  nogesgn1ores  27719  nosepnelem  27724  noinfbnd1lem3  27770  noinfbnd1lem5  27772  noinfbnd2lem1  27775  ttgval  28883  ttgbas  28887  ttgplusg  28889  ttgvsca  28892  ttgds  28894  cchhllem  28901  axlowdimlem13  28969  usgrexmpldifpr  29275  usgrexmplef  29276  vdegp1ai  29554  vdegp1bi  29555  konigsbergiedgw  30267  konigsberglem2  30272  konigsberglem3  30273  ex-pss  30447  ex-hash  30472  resvbas  33359  resvplusg  33361  resvmulr  33365  2sqr3minply  33791  signswch  34576  bj-disjsn01  36953  bj-1upln0  37010  finxpreclem3  37394  hlhilsbase  41942  hlhilsplus  41944  hlhilsmul  41946  aks6d1c7lem1  42181  ine1  42349  remul01  42437  sn-0tie0  42469  flt0  42647  mnuprdlem2  44292  ovnsubadd2lem  46660  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2nb2  47992  nnlog2ge0lt1  48487  logbpw2m1  48488  fllog2  48489  blennnelnn  48497  nnpw2blen  48501  blen1  48505  blen2  48506  blen1b  48509  blennnt2  48510  nnolog2flm1  48511  blennngt2o2  48513  blennn0e2  48515  inlinecirc02plem  48707