Theorem necon2ad 2670

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
necon2ad.1

Assertion

Ref	Expression
necon2ad

Proof of Theorem necon2ad

Step	Hyp	Ref	Expression
1		notnot1 122	. 2
2		necon2ad.1	. . 3
3	2	necon3bd 2669	. 2
4	1, 3	syl5 32	1

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