Theorem necomi 3013

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

This proof depends on syntax axioms:   ≠ wne 2959

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  nesymi  3016  nesymir  3017  0nep0  5323  opthhausdorff  5494  xp01disj  8527  xp01disjl  8528  enpr2d  9104  snnen2o  9264  rex2dom  9272  djuexb  10017  djuin  10026  pnfnemnf  11391  mnfnepnf  11392  ltneii  11450  0ne1  12441  0ne2  12579  xnn0n0n1ge2b  13288  xmulpnf1  13431  fzprval  13746  fvf1tp  13956  hashneq0  14535  f1oun2prg  15097  geo2sum2  16072  ressplusg  17491  ressmulr  17507  fnpr2o  17758  fvpr0o  17760  fvpr1o  17761  rescabs  18037  odubas  18494  degenmgmnfn  19165  degenmgm  19166  degenmgm2  19169  symgvalstruct  19641  dmdprdpr  20295  dprdpr  20296  mgpress  20400  rmodislmod  21235  sralem  21481  srasca  21485  sratset  21488  srads  21490  cnfldfun  21722  cnfldfunALT  21723  zlmbas  21853  zlmplusg  21854  zlmmulr  21855  zlmsca  21856  znbas2  21875  znadd  21876  znmul  21877  opsrbas  22389  opsrplusg  22390  opsrmulr  22391  opsrvsca  22392  opsrsca  22393  xpstopnlem1  24158  tuslem  24615  setsmsbas  24824  tngbas  24990  tngplusg  24991  tngmulr  24993  tngsca  24994  tngvsca  24995  tngip  24996  2logb9irrALT  27156  sqrt2cxp2logb9e3  27157  1sgm2ppw  27557  2sqlem11  27786  flt0  27999  nogesgn1ores  28061  nosepnelem  28066  noinfbnd1lem3  28112  noinfbnd1lem5  28114  noinfbnd2lem1  28117  ttgval  29482  ttgbas  29484  ttgplusg  29485  ttgvsca  29487  ttgds  29488  cchhllem  29494  axlowdimlem13  29562  usgrexmpldifpr  29869  usgrexmplef  29870  vdegp1ai  30147  vdegp1bi  30148  konigsbergiedgw  30879  konigsberglem2  30884  konigsberglem3  30885  ex-pss  31059  ex-hash  31084  resvbas  33965  resvplusg  33966  resvmulr  33968  2sqr3minply  34482  signswch  35260  bj-disjsn01  38043  bj-1upln0  38100  finxpreclem3  38508  hlhilsbase  43188  hlhilsplus  43189  hlhilsmul  43190  aks6d1c7lem1  43422  ine1  43564  remul01  43651  sn-0tie0  43708  mnuprdlem2  45449  ovnsubadd2lem  47860  usgrexmpl1lem  49324  usgrexmpl2lem  49329  usgrexmpl2nb2  49336  gpgprismgr4cycllem7  49404  nnlog2ge0lt1  49883  logbpw2m1  49884  fllog2  49885  blennnelnn  49893  nnpw2blen  49897  blen1  49901  blen2  49902  blen1b  49905  blennnt2  49906  nnolog2flm1  49907  blennngt2o2  49909  blennn0e2  49911  veronesev2lem  51254  veronesev3lem  51255  veronesevrowd  51259