Theorem necomi 2995

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

Syntax hints:   ≠ wne 2940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-ne 2941

This theorem is referenced by:  nesymi  2998  nesymir  2999  0nep0  5356  opthhausdorff  5517  xp01disj  8493  xp01disjl  8494  enpr2d  9051  snnen2o  9239  rex2dom  9248  1sdomOLD  9251  djuexb  9906  djuin  9915  pnfnemnf  11273  mnfnepnf  11274  ltneii  11331  0ne1  12287  0ne2  12423  xnn0n0n1ge2b  13115  xmulpnf1  13257  fzprval  13566  hashneq0  14328  f1oun2prg  14872  geo2sum2  15824  ressplusg  17239  ressmulr  17256  fnpr2o  17507  fvpr0o  17509  fvpr1o  17510  rescabs  17786  rescabsOLD  17787  odubas  18248  symgvalstruct  19305  symgvalstructOLD  19306  dmdprdpr  19960  dprdpr  19961  mgpress  20043  mgpressOLD  20044  rmodislmod  20684  sralem  20935  srasca  20943  sratset  20948  srads  20951  cnfldfun  21156  cnfldfunALT  21157  zlmbas  21287  zlmplusg  21289  zlmmulr  21291  zlmsca  21293  znbas2  21311  znadd  21313  znmul  21315  opsrbas  21825  opsrplusg  21827  opsrmulr  21829  opsrvsca  21831  opsrsca  21833  xpstopnlem1  23533  tuslem  23991  setsmsbas  24201  tngbas  24371  tngplusg  24373  tngmulr  24376  tngsca  24378  tngvsca  24380  tngip  24382  2logb9irrALT  26527  sqrt2cxp2logb9e3  26528  1sgm2ppw  26927  2sqlem11  27156  nogesgn1ores  27401  nosepnelem  27406  noinfbnd1lem3  27452  noinfbnd1lem5  27454  noinfbnd2lem1  27457  ttgval  28381  ttgbas  28385  ttgplusg  28387  ttgvsca  28390  ttgds  28392  cchhllem  28399  axlowdimlem13  28467  usgrexmpldifpr  28770  usgrexmplef  28771  vdegp1ai  29048  vdegp1bi  29049  konigsbergiedgw  29756  konigsberglem2  29761  konigsberglem3  29762  ex-pss  29936  ex-hash  29961  resvbas  32705  resvplusg  32707  resvmulr  32711  signswch  33858  gg-cnfldfun  35483  gg-cnfldfunALT  35484  bj-disjsn01  36136  bj-1upln0  36193  finxpreclem3  36577  hlhilsbase  41114  hlhilsplus  41116  hlhilsmul  41118  remul01  41582  sn-0tie0  41614  flt0  41681  mnuprdlem2  43334  ovnsubadd2lem  45660  nnlog2ge0lt1  47340  logbpw2m1  47341  fllog2  47342  blennnelnn  47350  nnpw2blen  47354  blen1  47358  blen2  47359  blen1b  47362  blennnt2  47363  nnolog2flm1  47364  blennngt2o2  47366  blennn0e2  47368  inlinecirc02plem  47560