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

Theorem necomi 2836
 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 2835 . 2 (𝐴𝐵𝐵𝐴)
31, 2mpbi 219 1 𝐵𝐴
 Colors of variables: wff setvar class Syntax hints:   ≠ wne 2780 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782 This theorem is referenced by:  nesymi  2839  nesymir  2840  0nep0  4762  xp01disj  7463  1sdom  8048  pnfnemnf  9973  mnfnepnf  9974  ltneii  10029  0ne1  10965  0ne2  11116  xnn0n0n1ge2b  11841  xmulpnf1  11976  fzprval  12271  hashneq0  13016  f1oun2prg  13512  geo2sum2  14444  fprodn0f  14561  xpscfn  16042  xpsc0  16043  xpsc1  16044  rescabs  16316  dmdprdpr  18271  dprdpr  18272  mgpress  18323  xpstopnlem1  21422  1sgm2ppw  24725  2sqlem11  24954  axlowdimlem13  25634  usgraexmpldifpr  25928  usgraexmplef  25929  constr3lem4  26175  ex-pss  26677  ex-hash  26702  signswch  29964  bj-disjsn01  32130  bj-1upln0  32190  finxpreclem3  32406  ovnsubadd2lem  39535  vdegp1ai-av  40752  vdegp1bi-av  40753  konigsbergiedgw  41416  konigsberglem2  41423  konigsberglem3  41424  nnlog2ge0lt1  42158  logbpw2m1  42159  fllog2  42160  blennnelnn  42168  nnpw2blen  42172  blen1  42176  blen2  42177  blen1b  42180  blennnt2  42181  nnolog2flm1  42182  blennngt2o2  42184  blennn0e2  42186
 Copyright terms: Public domain W3C validator