Theorem necomi 3009

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

This proof depends on syntax axioms:   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956

This theorem is used by:  nesymi  3012  nesymir  3013  0nep0  5318  opthhausdorff  5489  xp01disj  8499  xp01disjl  8500  enpr2d  9076  snnen2o  9236  rex2dom  9244  djuexb  9990  djuin  9999  pnfnemnf  11364  mnfnepnf  11365  ltneii  11423  0ne1  12414  0ne2  12552  xnn0n0n1ge2b  13261  xmulpnf1  13404  fzprval  13719  fvf1tp  13929  hashneq0  14508  f1oun2prg  15068  geo2sum2  16043  ressplusg  17462  ressmulr  17478  fnpr2o  17729  fvpr0o  17731  fvpr1o  17732  rescabs  18008  odubas  18465  degenmgmnfn  19136  degenmgm  19137  degenmgm2  19140  symgvalstruct  19611  dmdprdpr  20265  dprdpr  20266  mgpress  20370  rmodislmod  21205  sralem  21451  srasca  21455  sratset  21458  srads  21460  cnfldfun  21692  cnfldfunALT  21693  zlmbas  21823  zlmplusg  21824  zlmmulr  21825  zlmsca  21826  znbas2  21845  znadd  21846  znmul  21847  opsrbas  22359  opsrplusg  22360  opsrmulr  22361  opsrvsca  22362  opsrsca  22363  xpstopnlem1  24128  tuslem  24585  setsmsbas  24794  tngbas  24960  tngplusg  24961  tngmulr  24963  tngsca  24964  tngvsca  24965  tngip  24966  2logb9irrALT  27126  sqrt2cxp2logb9e3  27127  1sgm2ppw  27527  2sqlem11  27756  flt0  27969  nogesgn1ores  28031  nosepnelem  28036  noinfbnd1lem3  28082  noinfbnd1lem5  28084  noinfbnd2lem1  28087  ttgval  29452  ttgbas  29454  ttgplusg  29455  ttgvsca  29457  ttgds  29458  cchhllem  29464  axlowdimlem13  29532  usgrexmpldifpr  29839  usgrexmplef  29840  vdegp1ai  30117  vdegp1bi  30118  konigsbergiedgw  30849  konigsberglem2  30854  konigsberglem3  30855  ex-pss  31029  ex-hash  31054  resvbas  33895  resvplusg  33896  resvmulr  33898  2sqr3minply  34412  signswch  35190  bj-disjsn01  37865  bj-1upln0  37922  finxpreclem3  38317  hlhilsbase  42997  hlhilsplus  42998  hlhilsmul  42999  aks6d1c7lem1  43231  ine1  43372  remul01  43459  sn-0tie0  43516  mnuprdlem2  45257  ovnsubadd2lem  47655  usgrexmpl1lem  49119  usgrexmpl2lem  49124  usgrexmpl2nb2  49131  gpgprismgr4cycllem7  49199  nnlog2ge0lt1  49678  logbpw2m1  49679  fllog2  49680  blennnelnn  49688  nnpw2blen  49692  blen1  49696  blen2  49697  blen1b  49700  blennnt2  49701  nnolog2flm1  49702  blennngt2o2  49704  blennn0e2  49706  inlinecirc02plem  49898  veronesev2lem  50974  veronesev3lem  50975  veronesevrowd  50979