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

Theorem necomi 2844
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 2843 . 2 (𝐴𝐵𝐵𝐴)
31, 2mpbi 220 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:  wne 2790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-ne 2791
This theorem is referenced by:  nesymi  2847  nesymir  2848  0nep0  4806  xp01disj  7536  1sdom  8123  pnfnemnf  10054  mnfnepnf  10055  ltneii  10110  0ne1  11048  0ne2  11199  xnn0n0n1ge2b  11925  xmulpnf1  12063  fzprval  12359  hashneq0  13111  f1oun2prg  13614  geo2sum2  14549  fprodn0f  14666  xpscfn  16159  xpsc0  16160  xpsc1  16161  rescabs  16433  dmdprdpr  18388  dprdpr  18389  mgpress  18440  cnfldfunALT  19699  xpstopnlem1  21552  1sgm2ppw  24859  2sqlem11  25088  axlowdimlem13  25768  usgrexmpldifpr  26077  usgrexmplef  26078  vdegp1ai  26352  vdegp1bi  26353  konigsbergiedgw  27008  konigsberglem2  27015  konigsberglem3  27016  ex-pss  27173  ex-hash  27198  signswch  30460  nosepnelem  31618  bj-disjsn01  32637  bj-1upln0  32697  finxpreclem3  32901  ovnsubadd2lem  40196  nnlog2ge0lt1  41682  logbpw2m1  41683  fllog2  41684  blennnelnn  41692  nnpw2blen  41696  blen1  41700  blen2  41701  blen1b  41704  blennnt2  41705  nnolog2flm1  41706  blennngt2o2  41708  blennn0e2  41710
  Copyright terms: Public domain W3C validator