Theorem necon3bd 2669

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

Hypothesis

Ref	Expression
necon3bd.1

Assertion

Ref	Expression
necon3bd

Proof of Theorem necon3bd

Step	Hyp	Ref	Expression
1		nne 2658	. . 3
2		necon3bd.1	. . 3
3	1, 2	syl5bi 217	. 2
4	3	con1d 124	1

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

This theorem is referenced by:  necon2ad  2670  nelne1  2786  nelne2  2787  nssne1  3559  nssne2  3560  disjne  3872  difsn  4164  nbrne1  4469  nbrne2  4470  peano5  6723  oeeui  7270  domdifsn  7620  ac6sfi  7784  inf3lem2  8067  cnfcom3lem  8168  cnfcom3lemOLD  8176  dfac9  8537  fin23lem21  8740  dedekindle  9766  zneo  10970  modirr  12057  sqrmo  13085  pc2dvds  14402  pcadd  14408  4sqlem11  14473  latnlej  15698  sylow2blem3  16642  irredn0  17352  irredn1  17355  lssneln0  17598  lspsnne2  17764  lspfixed  17774  lspindpi  17778  lsmcv  17787  lspsolv  17789  isnzr2  17911  coe1tmmul  18318  dfac14  20119  fbdmn0  20335  filufint  20421  flimfnfcls  20529  alexsubALTlem2  20548  evth  21459  cphsqrtcl2  21633  ovolicc2lem4  21931  lhop1lem  22414  lhop1  22415  lhop2  22416  lhop  22417  deg1add  22504  abelthlem2  22827  logcnlem2  23024  angpined  23161  asinneg  23217  lgsne0  23608  lgsqr  23621  lgsquadlem2  23630  lgsquadlem3  23631  axlowdimlem17  24261  dvrunz  25435  spansncvi  26570  dmgmaddn0  28565  broutsideof2  29772  dvasin  30103  dvacos  30104  nninfnub  30244  pellexlem1  30765  dfac21  31012  pm13.14  31316  uzlidlring  32735  lsatcvatlem  34774  lkrlsp2  34828  opnlen0  34913  2llnne2N  35132  lnnat  35151  llnn0  35240  lplnn0N  35271  lplnllnneN  35280  llncvrlpln2  35281  llncvrlpln  35282  lvoln0N  35315  lplncvrlvol2  35339  lplncvrlvol  35340  dalempnes  35375  dalemqnet  35376  dalemcea  35384  dalem3  35388  cdlema1N  35515  cdlemb  35518  paddasslem5  35548  llnexchb2lem  35592  osumcllem4N  35683  pexmidlem1N  35694  lhp2lt  35725  lhp2atne  35758  lhp2at0ne  35760  4atexlemunv  35790  4atexlemex2  35795  trlne  35910  trlval4  35913  cdlemc4  35919  cdleme11dN  35987  cdleme11h  35991  cdlemednuN  36025  cdleme20j  36044  cdleme20k  36045  cdleme21at  36054  cdleme35f  36180  cdlemg11b  36368  dia2dimlem1  36791  dihmeetlem3N  37032  dihmeetlem15N  37048  dochsnnz  37177  dochexmidlem1  37187  dochexmidlem7  37193  mapdindp3  37449

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