Theorem necon3ad 2667

Description: Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)

Hypothesis

Ref	Expression
necon3ad.1

Assertion

Ref	Expression
necon3ad

Proof of Theorem necon3ad

Step	Hyp	Ref	Expression
1		necon3ad.1	. 2
2		id 22	. . 3
3	2	neneqd 2659	. 2
4	1, 3	nsyli 141	1

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

This theorem is referenced by:  necon1ad  2673  necon3d  2681  disjpss  3877  oeeulem  7269  enp1i  7775  canthp1lem2  9052  winalim2  9095  nlt1pi  9305  sqreulem  13192  rpnnen2lem11  13958  dvdseq  14033  eucalglt  14214  nprm  14231  pcprmpw2  14405  pcmpt  14411  expnprm  14421  prmlem0  14591  pltnle  15596  psgnunilem1  16518  pgpfi  16625  frgpnabllem1  16877  gsumval3a  16905  gsumval3aOLD  16906  ablfac1eulem  17123  pgpfaclem2  17133  lspdisjb  17772  lspdisj2  17773  obselocv  18759  0nnei  19613  t0dist  19826  t1sep  19871  ordthauslem  19884  hausflim  20482  bcthlem5  21767  bcth  21768  fta1g  22568  plyco0  22589  dgrnznn  22644  coeaddlem  22646  fta1  22704  vieta1lem2  22707  logcnlem3  23025  dvloglem  23029  dcubic  23177  mumullem2  23454  2sqlem8a  23646  dchrisum0flblem1  23693  colperpexlem2  24105  ocnel  26216  hatomistici  27281  sibfof  28282  outsideofrflx  29777  mblfinlem1  30051  cntotbnd  30292  heiborlem6  30312  2f1fvneq  32307  lshpnel  34708  lshpcmp  34713  lfl1  34795  lkrshp  34830  lkrpssN  34888  atnlt  35038  atnle  35042  atlatmstc  35044  intnatN  35131  atbtwn  35170  llnnlt  35247  lplnnlt  35289  2llnjaN  35290  lvolnltN  35342  2lplnja  35343  dalem-cly  35395  dalem44  35440  2llnma3r  35512  cdlemblem  35517  lhpm0atN  35753  lhp2atnle  35757  cdlemednpq  36024  cdleme22cN  36068  cdlemg18b  36405  cdlemg42  36455  dia2dimlem1  36791  dochkrshp  37113  hgmapval0  37622

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