Theorem necon1d 2682

Description: Contrapositive law deduction for inequality. (Contributed by NM, 28-Dec-2008.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypothesis

Ref	Expression
necon1d.1

Assertion

Ref	Expression
necon1d

Proof of Theorem necon1d

Step	Hyp	Ref	Expression
1		necon1d.1	. . 3
2		nne 2658	. . 3
3	1, 2	syl6ibr 227	. 2
4	3	necon4ad 2677	1

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

This theorem is referenced by:  disji  4440  mul02lem2  9778  xblss2ps  20904  xblss2  20905  lgsne0  23608  h1datomi  26499  eigorthi  26756  disjif  27439  lineintmo  29807  2llnmat  35248  2lnat  35508  tendospcanN  36750  dihmeetlem13N  37046  dochkrshp  37113

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