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

Theorem necomi 2986
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 2985 . 2 (𝐴𝐵𝐵𝐴)
31, 2mpbi 220 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:  wne 2932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-ne 2933
This theorem is referenced by:  nesymi  2989  nesymir  2990  0nep0  4985  opthhausdorff  5127  xp01disj  7745  1sdom  8328  djuin  8948  pnfnemnf  10286  mnfnepnf  10287  ltneii  10342  0ne1  11280  0ne2  11431  xnn0n0n1ge2b  12158  xmulpnf1  12297  fzprval  12594  hashneq0  13347  f1oun2prg  13862  geo2sum2  14804  fprodn0f  14921  xpscfn  16421  xpsc0  16422  xpsc1  16423  rescabs  16694  dmdprdpr  18648  dprdpr  18649  mgpress  18700  cnfldfunALT  19961  xpstopnlem1  21814  1sgm2ppw  25124  2sqlem11  25353  axlowdimlem13  26033  usgrexmpldifpr  26349  usgrexmplef  26350  vdegp1ai  26642  vdegp1bi  26643  konigsbergiedgw  27400  konigsberglem2  27405  konigsberglem3  27406  ex-pss  27596  ex-hash  27621  signswch  30947  nosepnelem  32136  bj-disjsn01  33243  bj-1upln0  33303  finxpreclem3  33541  ovnsubadd2lem  41365  nnlog2ge0lt1  42870  logbpw2m1  42871  fllog2  42872  blennnelnn  42880  nnpw2blen  42884  blen1  42888  blen2  42889  blen1b  42892  blennnt2  42893  nnolog2flm1  42894  blennngt2o2  42896  blennn0e2  42898
  Copyright terms: Public domain W3C validator