Theorem necon1bbii 2721

Description: Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)

Hypothesis

Ref	Expression
necon1bbii.1

Assertion

Ref	Expression
necon1bbii

Proof of Theorem necon1bbii

Step	Hyp	Ref	Expression
1		nne 2658	. 2
2		necon1bbii.1	. 2
3	1, 2	xchnxbi 308	1

Syntax hints:  -.wn 3  <->wb 184  =wceq 1395  =/=wne 2652

This theorem is referenced by:  necon2bbii  2724  rabeq0  3807  intnex  4609  class2set  4619  csbopab  4784  relimasn  5365  modom  7740  supval2  7935  fzo0  11849  vma1  23440  lgsquadlem3  23631  ordtconlem1  27906

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