Theorem pm2.61ine 2770

Description: Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
pm2.61ine.1
pm2.61ine.2

Assertion

Ref	Expression
pm2.61ine

Proof of Theorem pm2.61ine

Step	Hyp	Ref	Expression
1		pm2.61ine.2	. 2
2		nne 2658	. . 3
3		pm2.61ine.1	. . 3
4	2, 3	sylbi 195	. 2
5	1, 4	pm2.61i 164	1

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

This theorem is referenced by:  pm2.61ne  2772  pm2.61iine  2779  rgenz  3935  raaan  3937  raaanv  3938  iinrab2  4393  iinvdif  4402  riinrab  4406  reusv2lem2  4654  reusv6OLD  4663  reusv7OLD  4664  xpriindi  5144  dmxpid  5227  dmxpss  5443  rnxpid  5445  cnvpo  5550  xpcoid  5553  fnprb  6129  fconstfvOLD  6134  xpexr  6740  frxp  6910  suppimacnv  6929  fodomr  7688  wdompwdom  8025  en3lp  8054  inf3lemd  8065  prdom2  8405  iunfictbso  8516  infpssrlem4  8707  1re  9616  dedekindle  9766  00id  9776  nn0lt2  10952  nn01to3  11204  ioorebas  11655  fzfi  12082  ssnn0fi  12094  hash2prde  12516  repswsymballbi  12752  cshw0  12765  cshwmodn  12766  cshwsublen  12767  cshwn  12768  cshwlen  12770  cshwidx0  12776  cshwsidrepswmod0  14579  cshwshashlem1  14580  cshwshashlem2  14581  cshwsdisj  14583  cntzssv  16366  psgnunilem4  16522  mulmarep1gsum2  19076  plyssc  22597  axsegcon  24230  axpaschlem  24243  axlowdimlem16  24260  axcontlem7  24273  axcontlem8  24274  axcontlem12  24278  usgra2edg  24382  usgrcyclnl2  24641  4cycl4dv  24667  1to3vfriswmgra  25007  frgranbnb  25020  numclwwlk5  25112  siii  25768  h1de2ctlem  26473  riesz3i  26981  unierri  27023  dya2iocuni  28254  sibf0  28276  dfpo2  29184  cgrextend  29658  ifscgr  29694  idinside  29734  btwnconn1lem12  29748  btwnconn1  29751  linethru  29803  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  sdrgacs  31150  nrhmzr  32679  zlmodzxznm  33098  ax6e2ndeq  33332  bnj1143  33849  bnj571  33964  bnj594  33970  bnj852  33979  bj-xpnzex  34516

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