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

Theorem necomi 3070
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 3069 . 2 (𝐴𝐵𝐵𝐴)
31, 2mpbi 231 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:  wne 3016
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 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-ne 3017
This theorem is referenced by:  nesymi  3073  nesymir  3074  0nep0  5250  opthhausdorff  5399  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  19102  dprdpr  19103  mgpress  19181  cnfldfunALT  20488  xpstopnlem1  22347  2logb9irrALT  25303  sqrt2cxp2logb9e3  25304  1sgm2ppw  25704  2sqlem11  25933  axlowdimlem13  26668  usgrexmpldifpr  26968  usgrexmplef  26969  vdegp1ai  27246  vdegp1bi  27247  konigsbergiedgw  27955  konigsberglem2  27960  konigsberglem3  27961  ex-pss  28135  ex-hash  28160  signswch  31731  nosepnelem  33082  bj-disjsn01  34162  bj-1upln0  34219  finxpreclem3  34557  remul01  39117  mnuprdlem2  40489  ovnsubadd2lem  42808  nnlog2ge0lt1  44524  logbpw2m1  44525  fllog2  44526  blennnelnn  44534  nnpw2blen  44538  blen1  44542  blen2  44543  blen1b  44546  blennnt2  44547  nnolog2flm1  44548  blennngt2o2  44550  blennn0e2  44552  inlinecirc02plem  44671
  Copyright terms: Public domain W3C validator