Theorem necomi 2998

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

Syntax hints:   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ne 2944

This theorem is referenced by:  nesymi  3001  nesymir  3002  0nep0  5280  opthhausdorff  5431  xp01disj  8321  xp01disjl  8322  1sdom  9025  snnen2o  9026  djuexb  9667  djuin  9676  pnfnemnf  11030  mnfnepnf  11031  ltneii  11088  0ne1  12044  0ne2  12180  xnn0n0n1ge2b  12867  xmulpnf1  13008  fzprval  13317  hashneq0  14079  f1oun2prg  14630  geo2sum2  15586  ressplusg  17000  ressmulr  17017  fnpr2o  17268  fvpr0o  17270  fvpr1o  17271  rescabs  17547  rescabsOLD  17548  odubas  18009  symgvalstruct  19004  symgvalstructOLD  19005  dmdprdpr  19652  dprdpr  19653  mgpress  19735  mgpressOLD  19736  rmodislmod  20191  sralem  20439  srasca  20447  sratset  20452  srads  20455  cnfldfun  20609  cnfldfunALT  20610  zlmbas  20720  zlmplusg  20722  zlmmulr  20724  zlmsca  20726  znbas2  20744  znadd  20746  znmul  20748  opsrbas  21252  opsrplusg  21254  opsrmulr  21256  opsrvsca  21258  opsrsca  21260  xpstopnlem1  22960  tuslem  23418  setsmsbas  23628  tngbas  23798  tngplusg  23800  tngmulr  23803  tngsca  23805  tngvsca  23807  tngip  23809  2logb9irrALT  25948  sqrt2cxp2logb9e3  25949  1sgm2ppw  26348  2sqlem11  26577  ttgval  27236  ttgbas  27240  ttgplusg  27242  ttgvsca  27245  ttgds  27247  cchhllem  27254  axlowdimlem13  27322  usgrexmpldifpr  27625  usgrexmplef  27626  vdegp1ai  27903  vdegp1bi  27904  konigsbergiedgw  28612  konigsberglem2  28617  konigsberglem3  28618  ex-pss  28792  ex-hash  28817  resvbas  31532  resvplusg  31534  resvmulr  31538  signswch  32540  nogesgn1ores  33877  nosepnelem  33882  noinfbnd1lem3  33928  noinfbnd1lem5  33930  noinfbnd2lem1  33933  bj-disjsn01  35142  bj-1upln0  35199  finxpreclem3  35564  hlhilsbase  39954  hlhilsplus  39956  hlhilsmul  39958  remul01  40390  sn-0tie0  40421  flt0  40474  mnuprdlem2  41891  ovnsubadd2lem  44183  nnlog2ge0lt1  45912  logbpw2m1  45913  fllog2  45914  blennnelnn  45922  nnpw2blen  45926  blen1  45930  blen2  45931  blen1b  45934  blennnt2  45935  nnolog2flm1  45936  blennngt2o2  45938  blennn0e2  45940  inlinecirc02plem  46132