MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necomi Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 necomi.1 . 2 𝐴𝐵
2 necom 2996 . 2 (𝐴𝐵𝐵𝐴)
31, 2mpbi 229 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:  wne 2942
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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2730  df-ne 2943
This theorem is referenced by:  nesymi  3000  nesymir  3001  0nep0  5312  opthhausdorff  5472  xp01disj  8405  xp01disjl  8406  enpr2d  8927  snnen2o  9115  rex2dom  9124  1sdomOLD  9127  djuexb  9779  djuin  9788  pnfnemnf  11144  mnfnepnf  11145  ltneii  11202  0ne1  12158  0ne2  12294  xnn0n0n1ge2b  12981  xmulpnf1  13122  fzprval  13431  hashneq0  14192  f1oun2prg  14738  geo2sum2  15694  ressplusg  17106  ressmulr  17123  fnpr2o  17374  fvpr0o  17376  fvpr1o  17377  rescabs  17653  rescabsOLD  17654  odubas  18115  symgvalstruct  19110  symgvalstructOLD  19111  dmdprdpr  19757  dprdpr  19758  mgpress  19840  mgpressOLD  19841  rmodislmod  20313  sralem  20561  srasca  20569  sratset  20574  srads  20577  cnfldfun  20731  cnfldfunALT  20732  zlmbas  20842  zlmplusg  20844  zlmmulr  20846  zlmsca  20848  znbas2  20866  znadd  20868  znmul  20870  opsrbas  21374  opsrplusg  21376  opsrmulr  21378  opsrvsca  21380  opsrsca  21382  xpstopnlem1  23082  tuslem  23540  setsmsbas  23750  tngbas  23920  tngplusg  23922  tngmulr  23925  tngsca  23927  tngvsca  23929  tngip  23931  2logb9irrALT  26070  sqrt2cxp2logb9e3  26071  1sgm2ppw  26470  2sqlem11  26699  nogesgn1ores  26944  nosepnelem  26949  noinfbnd1lem3  26995  noinfbnd1lem5  26997  noinfbnd2lem1  27000  ttgval  27603  ttgbas  27607  ttgplusg  27609  ttgvsca  27612  ttgds  27614  cchhllem  27621  axlowdimlem13  27689  usgrexmpldifpr  27992  usgrexmplef  27993  vdegp1ai  28270  vdegp1bi  28271  konigsbergiedgw  28978  konigsberglem2  28983  konigsberglem3  28984  ex-pss  29158  ex-hash  29183  resvbas  31905  resvplusg  31907  resvmulr  31911  signswch  32934  bj-disjsn01  35309  bj-1upln0  35366  finxpreclem3  35750  hlhilsbase  40289  hlhilsplus  40291  hlhilsmul  40293  remul01  40723  sn-0tie0  40754  flt0  40809  mnuprdlem2  42286  ovnsubadd2lem  44594  nnlog2ge0lt1  46352  logbpw2m1  46353  fllog2  46354  blennnelnn  46362  nnpw2blen  46366  blen1  46370  blen2  46371  blen1b  46374  blennnt2  46375  nnolog2flm1  46376  blennngt2o2  46378  blennn0e2  46380  inlinecirc02plem  46572
  Copyright terms: Public domain W3C validator