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

Theorem necomi 3075
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 3074 . 2 (𝐴𝐵𝐵𝐴)
31, 2mpbi 231 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:  wne 3021
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2819  df-ne 3022
This theorem is referenced by:  nesymi  3078  nesymir  3079  0nep0  5255  opthhausdorff  5404  xp01disj  8111  xp01disjl  8112  1sdom  8710  djuexb  9327  djuin  9336  pnfnemnf  10685  mnfnepnf  10686  ltneii  10742  0ne1  11697  0ne2  11833  xnn0n0n1ge2b  12516  xmulpnf1  12657  fzprval  12958  hashneq0  13715  f1oun2prg  14269  geo2sum2  15220  fnpr2o  16820  fvpr0o  16822  fvpr1o  16823  rescabs  17093  dmdprdpr  19091  dprdpr  19092  mgpress  19170  cnfldfunALT  20474  xpstopnlem1  22333  2logb9irrALT  25289  sqrt2cxp2logb9e3  25290  1sgm2ppw  25690  2sqlem11  25919  axlowdimlem13  26654  usgrexmpldifpr  26954  usgrexmplef  26955  vdegp1ai  27232  vdegp1bi  27233  konigsbergiedgw  27941  konigsberglem2  27946  konigsberglem3  27947  ex-pss  28121  ex-hash  28146  signswch  31717  nosepnelem  33068  bj-disjsn01  34148  bj-1upln0  34205  finxpreclem3  34543  remul01  39102  mnuprdlem2  40474  ovnsubadd2lem  42793  nnlog2ge0lt1  44458  logbpw2m1  44459  fllog2  44460  blennnelnn  44468  nnpw2blen  44472  blen1  44476  blen2  44477  blen1b  44480  blennnt2  44481  nnolog2flm1  44482  blennngt2o2  44484  blennn0e2  44486  inlinecirc02plem  44605
  Copyright terms: Public domain W3C validator