Theorem necomi 3010

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

This proof depends on syntax axioms:   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ne 2957

This theorem is used by:  nesymi  3013  nesymir  3014  0nep0  5319  opthhausdorff  5490  xp01disj  8483  xp01disjl  8484  enpr2d  9060  snnen2o  9220  rex2dom  9228  djuexb  9971  djuin  9980  pnfnemnf  11345  mnfnepnf  11346  ltneii  11404  0ne1  12395  0ne2  12533  xnn0n0n1ge2b  13242  xmulpnf1  13385  fzprval  13699  fvf1tp  13909  hashneq0  14488  f1oun2prg  15048  geo2sum2  16023  ressplusg  17442  ressmulr  17458  fnpr2o  17709  fvpr0o  17711  fvpr1o  17712  rescabs  17988  odubas  18445  degenmgmnfn  19116  degenmgm  19117  degenmgm2  19120  symgvalstruct  19591  dmdprdpr  20245  dprdpr  20246  mgpress  20350  rmodislmod  21185  sralem  21431  srasca  21435  sratset  21438  srads  21440  cnfldfun  21672  cnfldfunALT  21673  zlmbas  21803  zlmplusg  21804  zlmmulr  21805  zlmsca  21806  znbas2  21825  znadd  21826  znmul  21827  opsrbas  22339  opsrplusg  22340  opsrmulr  22341  opsrvsca  22342  opsrsca  22343  xpstopnlem1  24108  tuslem  24565  setsmsbas  24774  tngbas  24940  tngplusg  24941  tngmulr  24943  tngsca  24944  tngvsca  24945  tngip  24946  2logb9irrALT  27108  sqrt2cxp2logb9e3  27109  1sgm2ppw  27509  2sqlem11  27738  flt0  27951  nogesgn1ores  28013  nosepnelem  28018  noinfbnd1lem3  28064  noinfbnd1lem5  28066  noinfbnd2lem1  28069  ttgval  29434  ttgbas  29436  ttgplusg  29437  ttgvsca  29439  ttgds  29440  cchhllem  29446  axlowdimlem13  29514  usgrexmpldifpr  29821  usgrexmplef  29822  vdegp1ai  30099  vdegp1bi  30100  konigsbergiedgw  30831  konigsberglem2  30836  konigsberglem3  30837  ex-pss  31011  ex-hash  31036  resvbas  33877  resvplusg  33878  resvmulr  33880  2sqr3minply  34394  signswch  35173  bj-disjsn01  37835  bj-1upln0  37892  finxpreclem3  38284  hlhilsbase  42964  hlhilsplus  42965  hlhilsmul  42966  aks6d1c7lem1  43198  ine1  43339  remul01  43426  sn-0tie0  43483  mnuprdlem2  45216  ovnsubadd2lem  47599  usgrexmpl1lem  49063  usgrexmpl2lem  49068  usgrexmpl2nb2  49075  gpgprismgr4cycllem7  49143  nnlog2ge0lt1  49622  logbpw2m1  49623  fllog2  49624  blennnelnn  49632  nnpw2blen  49636  blen1  49640  blen2  49641  blen1b  49644  blennnt2  49645  nnolog2flm1  49646  blennngt2o2  49648  blennn0e2  49650  inlinecirc02plem  49842  veronesev2lem  50918  veronesev3lem  50919  veronesevrowd  50923