Theorem necon3abii 2717

Description: Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)

Hypothesis

Ref	Expression
necon3abii.1

Assertion

Ref	Expression
necon3abii

Proof of Theorem necon3abii

Step	Hyp	Ref	Expression
1		df-ne 2654	. 2
2		necon3abii.1	. 2
3	1, 2	xchbinx 310	1

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

This theorem is referenced by:  necon3bbii  2718  necon3bii  2725  nesym  2729  n0f  3793  xpimasn  5457  rankxplim3  8320  rankxpsuc  8321  dflt2  11383  gcd0id  14161  axlowdimlem13  24257  filnetlem4  30199  pellex  30771  ldepspr  33074  dihatlat  37061  nev  37791

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