Theorem necon1ad 2673

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

Hypothesis

Ref	Expression
necon1ad.1

Assertion

Ref	Expression
necon1ad

Proof of Theorem necon1ad

Step	Hyp	Ref	Expression
1		necon1ad.1	. . 3
2	1	necon3ad 2667	. 2
3		notnot2 112	. 2
4	2, 3	syl6 33	1

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

This theorem is referenced by:  prnebg  4212  fr0  4863  sofld  5460  suppssOLD  6020  suppss2OLD  6530  onmindif2  6647  suppss  6949  suppss2  6953  uniinqs  7410  dfac5lem4  8528  uzwo  11173  seqf1olem1  12146  seqf1olem2  12147  hashnncl  12436  pceq0  14394  vdwmc2  14497  odcau  16624  islss  17581  fidomndrnglem  17955  mvrf1  18081  mpfrcl  18187  obs2ss  18760  obslbs  18761  dsmmacl  18772  regr1lem2  20241  iccpnfhmeo  21445  itg10a  22117  dvlip  22394  deg1ge  22499  elply2  22593  coeeulem  22621  dgrle  22640  coemullem  22647  basellem2  23355  perfectlem2  23505  lgsabs1  23609  lnon0  25713  atsseq  27266  disjif2  27442  suppss2f  27477  cvmseu  28721  itg2addnclem  30066  lsatcmp  34728  lsatcmp2  34729  ltrnnid  35860  trlatn0  35897  cdlemh  36543  dochlkr  37112

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