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

Theorem necomi 2831
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 2830 . 2 (𝐴𝐵𝐵𝐴)
31, 2mpbi 218 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:  wne 2775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-cleq 2598  df-ne 2777
This theorem is referenced by:  nesymi  2834  nesymir  2835  0nep0  4753  xp01disj  7436  1sdom  8021  ltneii  9997  0ne1  10931  0ne2  11082  pnfnemnf  11782  mnfnepnf  11783  xmulpnf1  11929  fzprval  12222  hashneq0  12964  f1oun2prg  13454  geo2sum2  14386  fprodn0f  14503  xpscfn  15984  xpsc0  15985  xpsc1  15986  rescabs  16258  dmdprdpr  18213  dprdpr  18214  mgpress  18265  xpstopnlem1  21360  1sgm2ppw  24638  2sqlem11  24867  axlowdimlem13  25548  usgraexmpldifpr  25690  usgraexmplef  25691  constr3lem4  25937  ex-pss  26439  ex-hash  26464  signswch  29766  bj-disjsn01  31929  bj-1upln0  31989  finxpreclem3  32205  ovnsubadd2lem  39335  xnn0n0n1ge2b  40214  vdegp1ai-av  40750  vdegp1bi-av  40751  konigsbergiedgw  41414  konigsberglem2  41421  konigsberglem3  41422  nnlog2ge0lt1  42156  logbpw2m1  42157  fllog2  42158  blennnelnn  42166  nnpw2blen  42170  blen1  42174  blen2  42175  blen1b  42178  blennnt2  42179  nnolog2flm1  42180  blennngt2o2  42182  blennn0e2  42184
  Copyright terms: Public domain W3C validator