Theorem necon3i 2697

Description: Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)

Hypothesis

Ref	Expression
necon3i.1

Assertion

Ref	Expression
necon3i

Proof of Theorem necon3i

Step	Hyp	Ref	Expression
1		necon3i.1	. . 3
2	1	necon3ai 2685	. 2
3	2	neqned 2660	1

Syntax hints:  ->wi 4  =wceq 1395  =/=wne 2652

This theorem is referenced by:  xpnz  5431  unixp  5545  inf3lem2  8067  infeq5  8075  cantnflem1  8129  cantnflem1OLD  8152  iunfictbso  8516  rankcf  9176  hashfun  12495  hashge3el3dif  12524  s1nz  12618  abssubne0  13149  expnprm  14421  grpn0  16082  pmtr3ncomlem2  16499  gsumval3OLD  16908  pgpfaclem2  17133  isdrng2  17406  mpfrcl  18187  ply1frcl  18355  gzrngunit  18483  zringunit  18520  zrngunit  18521  prmirredlem  18523  prmirredlemOLD  18526  uvcf1  18823  lindfrn  18856  dfac14lem  20118  flimclslem  20485  lebnumlem3  21463  pmltpclem2  21861  i1fmullem  22101  fta1glem1  22566  fta1blem  22569  dgrcolem1  22670  plydivlem4  22692  plyrem  22701  facth  22702  fta1lem  22703  vieta1lem1  22706  vieta1lem2  22707  vieta1  22708  aalioulem2  22729  geolim3  22735  logcj  22991  argregt0  22995  argimgt0  22997  argimlt0  22998  logneg2  23000  tanarg  23004  logtayl  23041  cxpsqrt  23084  cxpcn3lem  23121  cxpcn3  23122  dcubic2  23175  dcubic  23177  cubic  23180  asinlem  23199  atandmcj  23240  atancj  23241  atanlogsublem  23246  bndatandm  23260  birthdaylem1  23281  basellem4  23357  basellem5  23358  dchrn0  23525  lgsne0  23608  constr3lem2  24646  nmlno0lem  25708  nmlnop0iALT  26914  difneqnul  27415  cntnevol  28199  signsvtn0  28527  signstfveq0a  28533  signstfveq0  28534  nepss  29095  elima4  29209  heicant  30049  totbndbnd  30285  compne  31349  stoweidlem39  31821  cdleme3c  35955  cdleme7e  35972  imadisjlnd  37973

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