Theorem necon3d 2681

Description: Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)

Hypothesis

Ref	Expression
necon3d.1

Assertion

Ref	Expression
necon3d

Proof of Theorem necon3d

Step	Hyp	Ref	Expression
1		necon3d.1	. . 3
2	1	necon3ad 2667	. 2
3		df-ne 2654	. 2
4	2, 3	syl6ibr 227	1

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

This theorem is referenced by:  necon3iOLD  2698  pm13.18  2768  ssn0  3818  pssdifn0  3888  uniintsn  4324  suppssfvOLD  6531  suppssov1OLD  6532  ressuppssdif  6940  suppfnss  6944  suppssov1  6951  suppssfv  6955  omord  7236  nnmord  7300  mapdom2  7708  findcard2  7780  kmlem9  8559  isf32lem7  8760  1re  9616  addid1  9781  nn0n0n1ge2  10884  xnegdi  11469  fseqsupubi  12088  sqrtgt0  13092  supcvg  13667  ntrivcvgfvn0  13708  efne0  13832  pceulem  14369  pcqmul  14377  pcqcl  14380  pcaddlem  14407  pcadd  14408  grpinvnz  16109  symgfvne  16413  symg2bas  16423  odmulgeq  16579  gsumval3OLD  16908  gsumval3lem2  16910  gsumval3  16911  ring1ne0  17239  abvdom  17487  mptscmfsupp0  17576  lmodindp1  17660  lspsneleq  17761  lspsneq  17768  lspexch  17775  lspindp3  17782  lspsnsubn0  17786  ringelnzr  17914  0ringnnzr  17917  coe1tmmul2  18317  ply1scln0  18332  dsmmsubg  18774  dsmmlss  18775  elfrlmbasn0  18796  mavmulsolcl  19053  0ntr  19572  elcls3  19584  neindisj  19618  neindisj2  19624  conndisj  19917  dfcon2  19920  fbunfip  20370  deg1mul2  22515  ply1nzb  22523  ne0p  22604  dgreq0  22662  dgradd2  22665  dgrcolem2  22671  elqaalem3  22717  logcj  22991  argimgt0  22997  tanarg  23004  ang180lem2  23142  ftalem2  23347  ftalem4  23349  ftalem5  23350  dvdssqf  23412  lmimid  24159  lmiisolem  24161  hypcgrlem1  24164  hypcgrlem2  24165  f1otrg  24174  f1otrge  24175  ax5seglem4  24235  ax5seglem5  24236  axeuclid  24266  axcontlem2  24268  axcontlem4  24270  usgra2adedgspthlem2  24612  usgra2wlkspthlem1  24619  usgra2wlkspthlem2  24620  frgregordn0  25070  nmlno0lem  25708  hlipgt0  25830  h1dn0  26470  spansneleq  26488  h1datomi  26499  nmlnop0iALT  26914  superpos  27273  chirredi  27313  ogrpaddlt  27708  qqhval2lem  27962  derangenlem  28615  subfacp1lem5  28628  btwndiff  29677  btwnconn1lem7  29743  btwnconn1lem12  29748  tan2h  30047  dvcnsqrt  30101  areacirclem1  30107  isdrngo2  30361  isdrngo3  30362  pell1234qrne0  30789  jm2.26lem3  30943  2zrngnmlid  32755  2zrngnmrid  32756  2zrngnmlid2  32757  domnmsuppn0  32962  rmsuppss  32963  scmsuppss  32965  aacllem  33216  lsatn0  34724  lsatspn0  34725  lkrlspeqN  34896  cvlsupr2  35068  dalem25  35422  4atexlemcnd  35796  ltrncnvnid  35851  trlator0  35896  ltrnnidn  35899  trlnid  35904  cdleme3b  35954  cdleme11l  35994  cdleme16b  36004  cdleme35h2  36183  cdleme38n  36190  cdlemg8c  36355  cdlemg11a  36363  cdlemg12e  36373  cdlemg18a  36404  trlcoat  36449  trlcone  36454  tendo1ne0  36554  cdleml9  36710  dvheveccl  36839  dihmeetlem13N  37046  dihlspsnat  37060  dihpN  37063  dihatexv  37065  dochsat  37110  dochkrshp  37113  dochkr1  37205  lcfrlem28  37297  lcfrlem32  37301  mapdn0  37396  mapdpglem11  37409  mapdpglem16  37414

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