Theorem necomi 2987

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

Syntax hints:   ≠ wne 2933

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 2709

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

This theorem is referenced by:  nesymi  2990  nesymir  2991  0nep0  5300  opthhausdorff  5472  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  47314  usgrexmpl1lem  48491  usgrexmpl2lem  48496  usgrexmpl2nb2  48503  gpgprismgr4cycllem7  48571  nnlog2ge0lt1  49036  logbpw2m1  49037  fllog2  49038  blennnelnn  49046  nnpw2blen  49050  blen1  49054  blen2  49055  blen1b  49058  blennnt2  49059  nnolog2flm1  49060  blennngt2o2  49062  blennn0e2  49064  inlinecirc02plem  49256