Theorem necomi 2997

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

Syntax hints:   ≠ wne 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ne 2943

This theorem is referenced by:  nesymi  3000  nesymir  3001  0nep0  5275  opthhausdorff  5425  xp01disj  8287  xp01disjl  8288  1sdom  8955  djuexb  9598  djuin  9607  pnfnemnf  10961  mnfnepnf  10962  ltneii  11018  0ne1  11974  0ne2  12110  xnn0n0n1ge2b  12796  xmulpnf1  12937  fzprval  13246  hashneq0  14007  f1oun2prg  14558  geo2sum2  15514  ressplusg  16926  ressmulr  16943  fnpr2o  17185  fvpr0o  17187  fvpr1o  17188  rescabs  17464  symgvalstruct  18919  symgvalstructOLD  18920  dmdprdpr  19567  dprdpr  19568  mgpress  19650  mgpressOLD  19651  rmodislmod  20106  sralem  20354  sratset  20365  srads  20368  cnfldfunALT  20523  zlmbas  20632  zlmplusg  20634  zlmmulr  20636  zlmsca  20638  znbas2  20656  znadd  20658  znmul  20660  opsrbas  21162  opsrplusg  21164  opsrmulr  21166  opsrvsca  21168  opsrsca  21170  xpstopnlem1  22868  tuslem  23326  tngbas  23704  tngplusg  23706  tngmulr  23709  tngsca  23711  tngvsca  23713  tngip  23715  2logb9irrALT  25853  sqrt2cxp2logb9e3  25854  1sgm2ppw  26253  2sqlem11  26482  ttgbas  27143  ttgplusg  27145  ttgvsca  27148  ttgds  27150  cchhllem  27157  axlowdimlem13  27225  usgrexmpldifpr  27528  usgrexmplef  27529  vdegp1ai  27806  vdegp1bi  27807  konigsbergiedgw  28513  konigsberglem2  28518  konigsberglem3  28519  ex-pss  28693  ex-hash  28718  resvbas  31434  resvplusg  31436  resvmulr  31440  signswch  32440  nogesgn1ores  33804  nosepnelem  33809  noinfbnd1lem3  33855  noinfbnd1lem5  33857  noinfbnd2lem1  33860  bj-disjsn01  35069  bj-1upln0  35126  finxpreclem3  35491  hlhilsbase  39881  hlhilsplus  39883  hlhilsmul  39885  remul01  40311  sn-0tie0  40342  flt0  40390  mnuprdlem2  41780  ovnsubadd2lem  44073  nnlog2ge0lt1  45800  logbpw2m1  45801  fllog2  45802  blennnelnn  45810  nnpw2blen  45814  blen1  45818  blen2  45819  blen1b  45822  blennnt2  45823  nnolog2flm1  45824  blennngt2o2  45826  blennn0e2  45828  inlinecirc02plem  46020