Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon2ad Unicode version

 Description: Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
Hypothesis
Ref Expression
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  =/=wne 2652 This theorem is referenced by:  necon2d  2683  prneimg  4211  tz7.2  4868  nordeq  4902  omxpenlem  7638  pr2ne  8404  cflim2  8664  cfslb2n  8669  ltne  9702  sqrt2irr  13982  rpexp  14261  pcgcd1  14400  plttr  15600  odhash3  16596  lbspss  17728  nzrunit  17915  en2top  19487  fbfinnfr  20342  ufileu  20420  alexsubALTlem4  20550  lebnumlem1  21461  lebnumlem2  21462  lebnumlem3  21463  ivthlem2  21864  ivthlem3  21865  dvne0  22412  deg1nn0clb  22490  lgsmod  23596  axlowdimlem16  24260  normgt0  26044  nofulllem4  29465  lswn0  32343  islln2a  35241  islpln2a  35272  islvol2aN  35316  dalem1  35383  trlnidatb  35902 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 185  df-ne 2654