Theorem necomi 2982

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

Syntax hints:   ≠ wne 2928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2929

This theorem is referenced by:  nesymi  2985  nesymir  2986  0nep0  5296  opthhausdorff  5457  xp01disj  8406  xp01disjl  8407  enpr2d  8970  snnen2o  9129  rex2dom  9137  djuexb  9799  djuin  9808  pnfnemnf  11164  mnfnepnf  11165  ltneii  11223  0ne1  12193  0ne2  12324  xnn0n0n1ge2b  13028  xmulpnf1  13170  fzprval  13482  fvf1tp  13690  hashneq0  14268  f1oun2prg  14821  geo2sum2  15778  ressplusg  17192  ressmulr  17208  fnpr2o  17458  fvpr0o  17460  fvpr1o  17461  rescabs  17737  odubas  18194  symgvalstruct  19307  dmdprdpr  19961  dprdpr  19962  mgpress  20066  rmodislmod  20861  sralem  21108  srasca  21112  sratset  21115  srads  21117  cnfldfun  21303  cnfldfunALT  21304  cnfldfunOLD  21316  cnfldfunALTOLD  21317  zlmbas  21452  zlmplusg  21453  zlmmulr  21454  zlmsca  21455  znbas2  21474  znadd  21475  znmul  21476  opsrbas  21983  opsrplusg  21984  opsrmulr  21985  opsrvsca  21986  opsrsca  21987  xpstopnlem1  23722  tuslem  24179  setsmsbas  24388  tngbas  24554  tngplusg  24555  tngmulr  24557  tngsca  24558  tngvsca  24559  tngip  24560  2logb9irrALT  26733  sqrt2cxp2logb9e3  26734  1sgm2ppw  27136  2sqlem11  27365  nogesgn1ores  27611  nosepnelem  27616  noinfbnd1lem3  27662  noinfbnd1lem5  27664  noinfbnd2lem1  27667  ttgval  28851  ttgbas  28853  ttgplusg  28854  ttgvsca  28856  ttgds  28857  cchhllem  28863  axlowdimlem13  28930  usgrexmpldifpr  29234  usgrexmplef  29235  vdegp1ai  29513  vdegp1bi  29514  konigsbergiedgw  30223  konigsberglem2  30228  konigsberglem3  30229  ex-pss  30403  ex-hash  30428  resvbas  33294  resvplusg  33295  resvmulr  33297  2sqr3minply  33788  signswch  34569  bj-disjsn01  36985  bj-1upln0  37042  finxpreclem3  37426  hlhilsbase  41977  hlhilsplus  41978  hlhilsmul  41979  aks6d1c7lem1  42212  ine1  42346  remul01  42439  sn-0tie0  42483  flt0  42669  mnuprdlem2  44305  ovnsubadd2lem  46682  usgrexmpl1lem  48051  usgrexmpl2lem  48056  usgrexmpl2nb2  48063  gpgprismgr4cycllem7  48131  nnlog2ge0lt1  48597  logbpw2m1  48598  fllog2  48599  blennnelnn  48607  nnpw2blen  48611  blen1  48615  blen2  48616  blen1b  48619  blennnt2  48620  nnolog2flm1  48621  blennngt2o2  48623  blennn0e2  48625  inlinecirc02plem  48817