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

Theorem necomi 2996
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 2995 . 2 (𝐴𝐵𝐵𝐴)
31, 2mpbi 229 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:  wne 2941
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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2729  df-ne 2942
This theorem is referenced by:  nesymi  2999  nesymir  3000  0nep0  5311  opthhausdorff  5471  xp01disj  8404  xp01disjl  8405  enpr2d  8926  snnen2o  9114  rex2dom  9123  1sdomOLD  9126  djuexb  9778  djuin  9787  pnfnemnf  11143  mnfnepnf  11144  ltneii  11201  0ne1  12157  0ne2  12293  xnn0n0n1ge2b  12980  xmulpnf1  13121  fzprval  13430  hashneq0  14191  f1oun2prg  14737  geo2sum2  15693  ressplusg  17105  ressmulr  17122  fnpr2o  17373  fvpr0o  17375  fvpr1o  17376  rescabs  17652  rescabsOLD  17653  odubas  18114  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  27615  ttgbas  27619  ttgplusg  27621  ttgvsca  27624  ttgds  27626  cchhllem  27633  axlowdimlem13  27701  usgrexmpldifpr  28004  usgrexmplef  28005  vdegp1ai  28282  vdegp1bi  28283  konigsbergiedgw  28990  konigsberglem2  28995  konigsberglem3  28996  ex-pss  29170  ex-hash  29195  resvbas  31917  resvplusg  31919  resvmulr  31923  signswch  32946  bj-disjsn01  35318  bj-1upln0  35375  finxpreclem3  35759  hlhilsbase  40298  hlhilsplus  40300  hlhilsmul  40302  remul01  40744  sn-0tie0  40776  flt0  40840  mnuprdlem2  42317  ovnsubadd2lem  44639  nnlog2ge0lt1  46401  logbpw2m1  46402  fllog2  46403  blennnelnn  46411  nnpw2blen  46415  blen1  46419  blen2  46420  blen1b  46423  blennnt2  46424  nnolog2flm1  46425  blennngt2o2  46427  blennn0e2  46429  inlinecirc02plem  46621
  Copyright terms: Public domain W3C validator