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  5305  opthhausdorff  5473  xp01disj  8428  xp01disjl  8429  enpr2d  8997  snnen2o  9157  rex2dom  9165  djuexb  9833  djuin  9842  pnfnemnf  11199  mnfnepnf  11200  ltneii  11258  0ne1  12228  0ne2  12359  xnn0n0n1ge2b  13058  xmulpnf1  13201  fzprval  13513  fvf1tp  13721  hashneq0  14299  f1oun2prg  14852  geo2sum2  15809  ressplusg  17223  ressmulr  17239  fnpr2o  17490  fvpr0o  17492  fvpr1o  17493  rescabs  17769  odubas  18226  symgvalstruct  19338  dmdprdpr  19992  dprdpr  19993  mgpress  20097  rmodislmod  20893  sralem  21140  srasca  21144  sratset  21147  srads  21149  cnfldfun  21335  cnfldfunALT  21336  cnfldfunOLD  21348  cnfldfunALTOLD  21349  zlmbas  21484  zlmplusg  21485  zlmmulr  21486  zlmsca  21487  znbas2  21506  znadd  21507  znmul  21508  opsrbas  22017  opsrplusg  22018  opsrmulr  22019  opsrvsca  22020  opsrsca  22021  xpstopnlem1  23765  tuslem  24222  setsmsbas  24431  tngbas  24597  tngplusg  24598  tngmulr  24600  tngsca  24601  tngvsca  24602  tngip  24603  2logb9irrALT  26776  sqrt2cxp2logb9e3  26777  1sgm2ppw  27179  2sqlem11  27408  nogesgn1ores  27654  nosepnelem  27659  noinfbnd1lem3  27705  noinfbnd1lem5  27707  noinfbnd2lem1  27710  ttgval  28959  ttgbas  28961  ttgplusg  28962  ttgvsca  28964  ttgds  28965  cchhllem  28971  axlowdimlem13  29039  usgrexmpldifpr  29343  usgrexmplef  29344  vdegp1ai  29622  vdegp1bi  29623  konigsbergiedgw  30335  konigsberglem2  30340  konigsberglem3  30341  ex-pss  30515  ex-hash  30540  resvbas  33426  resvplusg  33427  resvmulr  33429  2sqr3minply  33957  signswch  34738  bj-disjsn01  37194  bj-1upln0  37251  finxpreclem3  37642  hlhilsbase  42309  hlhilsplus  42310  hlhilsmul  42311  aks6d1c7lem1  42544  ine1  42678  remul01  42771  sn-0tie0  42815  flt0  42989  mnuprdlem2  44623  ovnsubadd2lem  46997  nthrucw  47238  usgrexmpl1lem  48375  usgrexmpl2lem  48380  usgrexmpl2nb2  48387  gpgprismgr4cycllem7  48455  nnlog2ge0lt1  48920  logbpw2m1  48921  fllog2  48922  blennnelnn  48930  nnpw2blen  48934  blen1  48938  blen2  48939  blen1b  48942  blennnt2  48943  nnolog2flm1  48944  blennngt2o2  48946  blennn0e2  48948  inlinecirc02plem  49140