Theorem necomi 3012

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

Syntax hints:   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  nesymi  3015  nesymir  3016  0nep0  5330  opthhausdorff  5502  xp01disj  8477  xp01disjl  8478  enpr2d  9046  snnen2o  9206  rex2dom  9214  djuexb  9896  djuin  9905  pnfnemnf  11265  mnfnepnf  11266  ltneii  11324  0ne1  12313  0ne2  12451  xnn0n0n1ge2b  13158  xmulpnf1  13301  fzprval  13615  fvf1tp  13824  hashneq0  14402  f1oun2prg  14956  geo2sum2  15930  ressplusg  17345  ressmulr  17361  fnpr2o  17612  fvpr0o  17614  fvpr1o  17615  rescabs  17891  odubas  18348  symgvalstruct  19468  dmdprdpr  20122  dprdpr  20123  mgpress  20227  rmodislmod  21032  sralem  21278  srasca  21282  sratset  21285  srads  21287  cnfldfun  21517  cnfldfunALT  21518  zlmbas  21648  zlmplusg  21649  zlmmulr  21650  zlmsca  21651  znbas2  21670  znadd  21671  znmul  21672  opsrbas  22182  opsrplusg  22183  opsrmulr  22184  opsrvsca  22185  opsrsca  22186  xpstopnlem1  23947  tuslem  24404  setsmsbas  24613  tngbas  24779  tngplusg  24780  tngmulr  24782  tngsca  24783  tngvsca  24784  tngip  24785  2logb9irrALT  26941  sqrt2cxp2logb9e3  26942  1sgm2ppw  27342  2sqlem11  27571  nogesgn1ores  27816  nosepnelem  27821  noinfbnd1lem3  27867  noinfbnd1lem5  27869  noinfbnd2lem1  27872  ttgval  29202  ttgbas  29204  ttgplusg  29205  ttgvsca  29207  ttgds  29208  cchhllem  29214  axlowdimlem13  29282  usgrexmpldifpr  29586  usgrexmplef  29587  vdegp1ai  29864  vdegp1bi  29865  konigsbergiedgw  30577  konigsberglem2  30582  konigsberglem3  30583  ex-pss  30757  ex-hash  30782  resvbas  33632  resvplusg  33633  resvmulr  33635  2sqr3minply  34148  signswch  34926  bj-disjsn01  37566  bj-1upln0  37623  finxpreclem3  38017  hlhilsbase  42691  hlhilsplus  42692  hlhilsmul  42693  aks6d1c7lem1  42925  ine1  43053  remul01  43146  sn-0tie0  43203  flt0  43349  mnuprdlem2  44963  ovnsubadd2lem  47339  nthrucw  47582  usgrexmpl1lem  48763  usgrexmpl2lem  48768  usgrexmpl2nb2  48775  gpgprismgr4cycllem7  48843  nnlog2ge0lt1  49323  logbpw2m1  49324  fllog2  49325  blennnelnn  49333  nnpw2blen  49337  blen1  49341  blen2  49342  blen1b  49345  blennnt2  49346  nnolog2flm1  49347  blennngt2o2  49349  blennn0e2  49351  inlinecirc02plem  49543