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

Theorem necomi 3067
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 3066 . 2 (𝐴𝐵𝐵𝐴)
31, 2mpbi 231 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:  wne 3013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-ne 3014
This theorem is referenced by:  nesymi  3070  nesymir  3071  0nep0  5249  opthhausdorff  5398  xp01disj  8109  xp01disjl  8110  1sdom  8709  djuexb  9326  djuin  9335  pnfnemnf  10684  mnfnepnf  10685  ltneii  10741  0ne1  11696  0ne2  11832  xnn0n0n1ge2b  12514  xmulpnf1  12655  fzprval  12956  hashneq0  13713  f1oun2prg  14267  geo2sum2  15218  fnpr2o  16818  fvpr0o  16820  fvpr1o  16821  rescabs  17091  dmdprdpr  19100  dprdpr  19101  mgpress  19179  cnfldfunALT  20486  xpstopnlem1  22345  2logb9irrALT  25303  sqrt2cxp2logb9e3  25304  1sgm2ppw  25703  2sqlem11  25932  axlowdimlem13  26667  usgrexmpldifpr  26967  usgrexmplef  26968  vdegp1ai  27245  vdegp1bi  27246  konigsbergiedgw  27954  konigsberglem2  27959  konigsberglem3  27960  ex-pss  28134  ex-hash  28159  signswch  31730  nosepnelem  33081  bj-disjsn01  34161  bj-1upln0  34218  finxpreclem3  34556  remul01  39115  mnuprdlem2  40486  ovnsubadd2lem  42804  nnlog2ge0lt1  44554  logbpw2m1  44555  fllog2  44556  blennnelnn  44564  nnpw2blen  44568  blen1  44572  blen2  44573  blen1b  44576  blennnt2  44577  nnolog2flm1  44578  blennngt2o2  44580  blennn0e2  44582  inlinecirc02plem  44701
  Copyright terms: Public domain W3C validator