Theorem necomi 3015

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

This proof depends on syntax axioms:   ≠ wne 2961

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ne 2962

This theorem is used by:  nesymi  3018  nesymir  3019  0nep0  5333  opthhausdorff  5505  xp01disj  8485  xp01disjl  8486  enpr2d  9055  snnen2o  9215  rex2dom  9223  djuexb  9914  djuin  9923  pnfnemnf  11282  mnfnepnf  11283  ltneii  11341  0ne1  12330  0ne2  12468  xnn0n0n1ge2b  13175  xmulpnf1  13318  fzprval  13632  fvf1tp  13842  hashneq0  14420  f1oun2prg  14980  geo2sum2  15954  ressplusg  17369  ressmulr  17385  fnpr2o  17636  fvpr0o  17638  fvpr1o  17639  rescabs  17915  odubas  18372  symgvalstruct  19498  dmdprdpr  20152  dprdpr  20153  mgpress  20257  rmodislmod  21088  sralem  21334  srasca  21338  sratset  21341  srads  21343  cnfldfun  21573  cnfldfunALT  21574  zlmbas  21704  zlmplusg  21705  zlmmulr  21706  zlmsca  21707  znbas2  21726  znadd  21727  znmul  21728  opsrbas  22238  opsrplusg  22239  opsrmulr  22240  opsrvsca  22241  opsrsca  22242  xpstopnlem1  24003  tuslem  24460  setsmsbas  24669  tngbas  24835  tngplusg  24836  tngmulr  24838  tngsca  24839  tngvsca  24840  tngip  24841  2logb9irrALT  27000  sqrt2cxp2logb9e3  27001  1sgm2ppw  27401  2sqlem11  27630  nogesgn1ores  27875  nosepnelem  27880  noinfbnd1lem3  27926  noinfbnd1lem5  27928  noinfbnd2lem1  27931  ttgval  29261  ttgbas  29263  ttgplusg  29264  ttgvsca  29266  ttgds  29267  cchhllem  29273  axlowdimlem13  29341  usgrexmpldifpr  29645  usgrexmplef  29646  vdegp1ai  29923  vdegp1bi  29924  konigsbergiedgw  30636  konigsberglem2  30641  konigsberglem3  30642  ex-pss  30816  ex-hash  30841  resvbas  33685  resvplusg  33686  resvmulr  33688  2sqr3minply  34201  signswch  34979  bj-disjsn01  37628  bj-1upln0  37685  finxpreclem3  38079  hlhilsbase  42753  hlhilsplus  42754  hlhilsmul  42755  aks6d1c7lem1  42987  ine1  43115  remul01  43208  sn-0tie0  43265  flt0  43409  mnuprdlem2  45023  ovnsubadd2lem  47399  usgrexmpl1lem  48826  usgrexmpl2lem  48831  usgrexmpl2nb2  48838  gpgprismgr4cycllem7  48906  nnlog2ge0lt1  49386  logbpw2m1  49387  fllog2  49388  blennnelnn  49396  nnpw2blen  49400  blen1  49404  blen2  49405  blen1b  49408  blennnt2  49409  nnolog2flm1  49410  blennngt2o2  49412  blennn0e2  49414  inlinecirc02plem  49606