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  8502  xp01disjl  8503  enpr2d  9079  snnen2o  9239  rex2dom  9247  djuexb  9993  djuin  10002  pnfnemnf  11367  mnfnepnf  11368  ltneii  11426  0ne1  12417  0ne2  12555  xnn0n0n1ge2b  13264  xmulpnf1  13407  fzprval  13722  fvf1tp  13932  hashneq0  14511  f1oun2prg  15073  geo2sum2  16048  ressplusg  17467  ressmulr  17483  fnpr2o  17734  fvpr0o  17736  fvpr1o  17737  rescabs  18013  odubas  18470  degenmgmnfn  19141  degenmgm  19142  degenmgm2  19145  symgvalstruct  19616  dmdprdpr  20270  dprdpr  20271  mgpress  20375  rmodislmod  21210  sralem  21456  srasca  21460  sratset  21463  srads  21465  cnfldfun  21697  cnfldfunALT  21698  zlmbas  21828  zlmplusg  21829  zlmmulr  21830  zlmsca  21831  znbas2  21850  znadd  21851  znmul  21852  opsrbas  22364  opsrplusg  22365  opsrmulr  22366  opsrvsca  22367  opsrsca  22368  xpstopnlem1  24133  tuslem  24590  setsmsbas  24799  tngbas  24965  tngplusg  24966  tngmulr  24968  tngsca  24969  tngvsca  24970  tngip  24971  2logb9irrALT  27131  sqrt2cxp2logb9e3  27132  1sgm2ppw  27532  2sqlem11  27761  flt0  27974  nogesgn1ores  28036  nosepnelem  28041  noinfbnd1lem3  28087  noinfbnd1lem5  28089  noinfbnd2lem1  28092  ttgval  29457  ttgbas  29459  ttgplusg  29460  ttgvsca  29462  ttgds  29463  cchhllem  29469  axlowdimlem13  29537  usgrexmpldifpr  29844  usgrexmplef  29845  vdegp1ai  30122  vdegp1bi  30123  konigsbergiedgw  30854  konigsberglem2  30859  konigsberglem3  30860  ex-pss  31034  ex-hash  31059  resvbas  33941  resvplusg  33942  resvmulr  33944  2sqr3minply  34458  signswch  35236  bj-disjsn01  37957  bj-1upln0  38014  finxpreclem3  38409  hlhilsbase  43089  hlhilsplus  43090  hlhilsmul  43091  aks6d1c7lem1  43323  ine1  43464  remul01  43551  sn-0tie0  43608  mnuprdlem2  45350  ovnsubadd2lem  47748  usgrexmpl1lem  49212  usgrexmpl2lem  49217  usgrexmpl2nb2  49224  gpgprismgr4cycllem7  49292  nnlog2ge0lt1  49771  logbpw2m1  49772  fllog2  49773  blennnelnn  49781  nnpw2blen  49785  blen1  49789  blen2  49790  blen1b  49793  blennnt2  49794  nnolog2flm1  49795  blennngt2o2  49797  blennn0e2  49799  veronesev2lem  51142  veronesev3lem  51143  veronesevrowd  51147