Theorem necomi 3014

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

Syntax hints:   ≠ wne 2960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ne 2961

This theorem is referenced by:  nesymi  3017  nesymir  3018  0nep0  5319  opthhausdorff  5491  xp01disj  8464  xp01disjl  8465  enpr2d  9033  snnen2o  9193  rex2dom  9201  djuexb  9883  djuin  9892  pnfnemnf  11252  mnfnepnf  11253  ltneii  11311  0ne1  12303  0ne2  12441  xnn0n0n1ge2b  13148  xmulpnf1  13291  fzprval  13604  fvf1tp  13813  hashneq0  14391  f1oun2prg  14944  geo2sum2  15918  ressplusg  17334  ressmulr  17350  fnpr2o  17601  fvpr0o  17603  fvpr1o  17604  rescabs  17880  odubas  18337  symgvalstruct  19458  dmdprdpr  20112  dprdpr  20113  mgpress  20217  rmodislmod  21020  sralem  21266  srasca  21270  sratset  21273  srads  21275  cnfldfun  21496  cnfldfunALT  21497  zlmbas  21627  zlmplusg  21628  zlmmulr  21629  zlmsca  21630  znbas2  21649  znadd  21650  znmul  21651  opsrbas  22161  opsrplusg  22162  opsrmulr  22163  opsrvsca  22164  opsrsca  22165  xpstopnlem1  23927  tuslem  24384  setsmsbas  24593  tngbas  24759  tngplusg  24760  tngmulr  24762  tngsca  24763  tngvsca  24764  tngip  24765  2logb9irrALT  26921  sqrt2cxp2logb9e3  26922  1sgm2ppw  27322  2sqlem11  27551  nogesgn1ores  27796  nosepnelem  27801  noinfbnd1lem3  27847  noinfbnd1lem5  27849  noinfbnd2lem1  27852  ttgval  29133  ttgbas  29135  ttgplusg  29136  ttgvsca  29138  ttgds  29139  cchhllem  29145  axlowdimlem13  29213  usgrexmpldifpr  29517  usgrexmplef  29518  vdegp1ai  29795  vdegp1bi  29796  konigsbergiedgw  30508  konigsberglem2  30513  konigsberglem3  30514  ex-pss  30688  ex-hash  30713  resvbas  33569  resvplusg  33570  resvmulr  33572  2sqr3minply  34087  signswch  34865  bj-disjsn01  37449  bj-1upln0  37506  finxpreclem3  37899  hlhilsbase  42575  hlhilsplus  42576  hlhilsmul  42577  aks6d1c7lem1  42809  ine1  42935  remul01  43028  sn-0tie0  43085  flt0  43231  mnuprdlem2  44847  ovnsubadd2lem  47217  nthrucw  47460  usgrexmpl1lem  48641  usgrexmpl2lem  48646  usgrexmpl2nb2  48653  gpgprismgr4cycllem7  48721  nnlog2ge0lt1  49197  logbpw2m1  49198  fllog2  49199  blennnelnn  49207  nnpw2blen  49211  blen1  49215  blen2  49216  blen1b  49219  blennnt2  49220  nnolog2flm1  49221  blennngt2o2  49223  blennn0e2  49225  inlinecirc02plem  49417