Theorem necon4bd 2679

Description: Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)

Hypothesis

Ref	Expression
necon4bd.1

Assertion

Ref	Expression
necon4bd

Proof of Theorem necon4bd

Step	Hyp	Ref	Expression
1		necon4bd.1	. . 3
2	1	necon2bd 2672	. 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:  om00  7243  pw2f1olem  7641  xlt2add  11481  hashfun  12495  hashtpg  12523  fsumcl2lem  13553  fprodcl2lem  13757  gcdeq0  14159  phibndlem  14300  abvn0b  17951  cfinufil  20429  isxmet2d  20830  i1fres  22112  tdeglem4  22458  ply1domn  22524  pilem2  22847  isnsqf  23409  ppieq0  23450  chpeq0  23483  chteq0  23484  lcmeq0  31206  bcc0  31245  ltrnatlw  35908

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