Theorem necomi 2996

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

Syntax hints:   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  nesymi  2999  nesymir  3000  0nep0  5357  opthhausdorff  5518  xp01disj  8491  xp01disjl  8492  enpr2d  9049  snnen2o  9237  rex2dom  9246  1sdomOLD  9249  djuexb  9904  djuin  9913  pnfnemnf  11269  mnfnepnf  11270  ltneii  11327  0ne1  12283  0ne2  12419  xnn0n0n1ge2b  13111  xmulpnf1  13253  fzprval  13562  hashneq0  14324  f1oun2prg  14868  geo2sum2  15820  ressplusg  17235  ressmulr  17252  fnpr2o  17503  fvpr0o  17505  fvpr1o  17506  rescabs  17782  rescabsOLD  17783  odubas  18244  symgvalstruct  19264  symgvalstructOLD  19265  dmdprdpr  19919  dprdpr  19920  mgpress  20002  mgpressOLD  20003  rmodislmod  20540  sralem  20790  srasca  20798  sratset  20803  srads  20806  cnfldfun  20956  cnfldfunALT  20957  zlmbas  21068  zlmplusg  21070  zlmmulr  21072  zlmsca  21074  znbas2  21092  znadd  21094  znmul  21096  opsrbas  21606  opsrplusg  21608  opsrmulr  21610  opsrvsca  21612  opsrsca  21614  xpstopnlem1  23313  tuslem  23771  setsmsbas  23981  tngbas  24151  tngplusg  24153  tngmulr  24156  tngsca  24158  tngvsca  24160  tngip  24162  2logb9irrALT  26303  sqrt2cxp2logb9e3  26304  1sgm2ppw  26703  2sqlem11  26932  nogesgn1ores  27177  nosepnelem  27182  noinfbnd1lem3  27228  noinfbnd1lem5  27230  noinfbnd2lem1  27233  ttgval  28157  ttgbas  28161  ttgplusg  28163  ttgvsca  28166  ttgds  28168  cchhllem  28175  axlowdimlem13  28243  usgrexmpldifpr  28546  usgrexmplef  28547  vdegp1ai  28824  vdegp1bi  28825  konigsbergiedgw  29532  konigsberglem2  29537  konigsberglem3  29538  ex-pss  29712  ex-hash  29737  resvbas  32478  resvplusg  32480  resvmulr  32484  signswch  33603  gg-cnfldfun  35228  gg-cnfldfunALT  35229  bj-disjsn01  35881  bj-1upln0  35938  finxpreclem3  36322  hlhilsbase  40859  hlhilsplus  40861  hlhilsmul  40863  remul01  41328  sn-0tie0  41360  flt0  41427  mnuprdlem2  43080  ovnsubadd2lem  45409  nnlog2ge0lt1  47300  logbpw2m1  47301  fllog2  47302  blennnelnn  47310  nnpw2blen  47314  blen1  47318  blen2  47319  blen1b  47322  blennnt2  47323  nnolog2flm1  47324  blennngt2o2  47326  blennn0e2  47328  inlinecirc02plem  47520