Theorem necomi 2986

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

Syntax hints:   ≠ wne 2932

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ne 2933

This theorem is referenced by:  nesymi  2989  nesymir  2990  0nep0  5299  opthhausdorff  5471  xp01disj  8426  xp01disjl  8427  enpr2d  8995  snnen2o  9155  rex2dom  9163  djuexb  9833  djuin  9842  pnfnemnf  11200  mnfnepnf  11201  ltneii  11259  0ne1  12252  0ne2  12383  xnn0n0n1ge2b  13083  xmulpnf1  13226  fzprval  13539  fvf1tp  13748  hashneq0  14326  f1oun2prg  14879  geo2sum2  15839  ressplusg  17254  ressmulr  17270  fnpr2o  17521  fvpr0o  17523  fvpr1o  17524  rescabs  17800  odubas  18257  symgvalstruct  19372  dmdprdpr  20026  dprdpr  20027  mgpress  20131  rmodislmod  20925  sralem  21171  srasca  21175  sratset  21178  srads  21180  cnfldfun  21366  cnfldfunALT  21367  zlmbas  21497  zlmplusg  21498  zlmmulr  21499  zlmsca  21500  znbas2  21519  znadd  21520  znmul  21521  opsrbas  22028  opsrplusg  22029  opsrmulr  22030  opsrvsca  22031  opsrsca  22032  xpstopnlem1  23774  tuslem  24231  setsmsbas  24440  tngbas  24606  tngplusg  24607  tngmulr  24609  tngsca  24610  tngvsca  24611  tngip  24612  2logb9irrALT  26762  sqrt2cxp2logb9e3  26763  1sgm2ppw  27163  2sqlem11  27392  nogesgn1ores  27638  nosepnelem  27643  noinfbnd1lem3  27689  noinfbnd1lem5  27691  noinfbnd2lem1  27694  ttgval  28943  ttgbas  28945  ttgplusg  28946  ttgvsca  28948  ttgds  28949  cchhllem  28955  axlowdimlem13  29023  usgrexmpldifpr  29327  usgrexmplef  29328  vdegp1ai  29605  vdegp1bi  29606  konigsbergiedgw  30318  konigsberglem2  30323  konigsberglem3  30324  ex-pss  30498  ex-hash  30523  resvbas  33394  resvplusg  33395  resvmulr  33397  2sqr3minply  33924  signswch  34705  bj-disjsn01  37259  bj-1upln0  37316  finxpreclem3  37709  hlhilsbase  42385  hlhilsplus  42386  hlhilsmul  42387  aks6d1c7lem1  42619  ine1  42746  remul01  42839  sn-0tie0  42896  flt0  43070  mnuprdlem2  44700  ovnsubadd2lem  47073  nthrucw  47316  usgrexmpl1lem  48497  usgrexmpl2lem  48502  usgrexmpl2nb2  48509  gpgprismgr4cycllem7  48577  nnlog2ge0lt1  49042  logbpw2m1  49043  fllog2  49044  blennnelnn  49052  nnpw2blen  49056  blen1  49060  blen2  49061  blen1b  49064  blennnt2  49065  nnolog2flm1  49066  blennngt2o2  49068  blennn0e2  49070  inlinecirc02plem  49262