Theorem necon3bii 2725

Description: Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)

Hypothesis

Ref	Expression
necon3bii.1

Assertion

Ref	Expression
necon3bii

Proof of Theorem necon3bii

Step	Hyp	Ref	Expression
1		necon3bii.1	. . 3
2	1	necon3abii 2717	. 2
3		df-ne 2654	. 2
4	2, 3	bitr4i 252	1

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

This theorem is referenced by:  necom  2726  neeq1i  2742  neeq2i  2744  neeq12i  2746  rnsnn0  5479  onoviun  7033  onnseq  7034  intrnfi  7896  wdomtr  8022  noinfep  8097  noinfepOLD  8098  wemapwe  8160  wemapweOLD  8161  scott0s  8327  cplem1  8328  karden  8334  acndom2  8456  dfac5lem3  8527  fin23lem31  8744  fin23lem40  8752  isf34lem5  8779  isf34lem7  8780  isf34lem6  8781  axrrecex  9561  negne0bi  9915  rpnnen1lem4  11240  rpnnen1lem5  11241  fseqsupcl  12087  limsupgre  13304  isercolllem3  13489  rpnnen2  13959  ruclem11  13973  3dvds  14050  prmreclem6  14439  0ram  14538  0ram2  14539  0ramcl  14541  gsumval2  15907  ghmrn  16280  gexex  16859  gsumval3OLD  16908  gsumval3  16911  iinopn  19411  cnconn  19923  1stcfb  19946  qtopeu  20217  fbasrn  20385  alexsublem  20544  evth  21459  minveclem1  21839  minveclem3b  21843  ovollb2  21900  ovolunlem1a  21907  ovolunlem1  21908  ovoliunlem1  21913  ovoliun2  21917  ioombl1lem4  21971  uniioombllem1  21990  uniioombllem2  21992  uniioombllem6  21997  mbfsup  22071  mbfinf  22072  mbflimsup  22073  itg1climres  22121  itg2monolem1  22157  itg2mono  22160  itg2i1fseq2  22163  sincos4thpi  22906  axlowdimlem13  24257  eupath  24981  siii  25768  minvecolem1  25790  bcsiALT  26096  h1de2bi  26472  h1de2ctlem  26473  nmlnopgt0i  26916  rge0scvg  27931  erdszelem5  28639  cvmsss2  28719  elrn3  29192  rankeq1o  29828  fin2so  30040  heicant  30049  scottn0f  30578  fnwe2lem2  30997  wnefimgd  37974

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