Theorem eqnetrd 2750

Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)

Hypotheses

Ref	Expression
eqnetrd.1
eqnetrd.2

Assertion

Ref	Expression
eqnetrd

Proof of Theorem eqnetrd

Step	Hyp	Ref	Expression
1		eqnetrd.2	. 2
2		eqnetrd.1	. . 3
3	2	neeq1d 2734	. 2
4	1, 3	mpbird 232	1

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

This theorem is referenced by:  eqnetrrd  2751  3netr4d  2762  opnz  4723  frsn  5075  xpdifid  5440  xpimasnOLD  5458  undefne0  7027  onoviun  7033  intrnfi  7896  cantnfp1lem2  8119  cantnfp1lem3  8120  cantnfp1lem2OLD  8145  cantnfp1lem3OLD  8146  wemapwe  8160  wemapweOLD  8161  acndom2  8456  fin23lem14  8734  fin23lem40  8752  isf32lem6  8759  isf34lem5  8779  isf34lem7  8780  isf34lem6  8781  axcc2lem  8837  xaddnemnf  11462  xaddnepnf  11463  fseqsupcl  12087  hashprg  12460  elprchashprn2  12461  limsupgre  13304  isercolllem3  13489  prodfn0  13703  ntrivcvgtail  13709  fproddiv  13766  fprodn0  13783  tanval3  13869  tanneg  13883  ruclem11  13973  phibndlem  14300  dfphi2  14304  0ram  14538  0ram2  14539  ram0  14540  0ramcl  14541  gsumval2  15907  sgrp2nmndlem5  16047  issubg2  16216  ghmrn  16280  pmtrmvd  16481  gsumval3OLD  16908  gsumval3  16911  pgpfaclem2  17133  ablfaclem2  17137  ablfaclem3  17138  abvdom  17487  lbsextlem2  17805  gzrngunit  18483  zringunit  18520  zrngunit  18521  cnmsgnsubg  18613  frlmssuvc2  18826  frlmssuvc2OLD  18828  iinopn  19411  cnconn  19923  1stcfb  19946  dissnlocfin  20030  fbasrn  20385  fclscmpi  20530  alexsublem  20544  ustuqtop5  20748  cnextucn  20806  dscmet  21093  reperflem  21323  evth  21459  cmetcaulem  21727  iscmet3  21732  cmetss  21753  bcthlem5  21767  bcth2  21769  mbflimsup  22073  itg1addlem4  22106  itg1climres  22121  itg2monolem1  22157  itg2i1fseq2  22163  tdeglem4  22458  deg1add  22504  deg1mul2  22515  deg1tm  22519  dgreq  22641  dgradd2  22665  dgrmul  22667  dgrmulc  22668  dgrcolem1  22670  plyrem  22701  facth  22702  fta1lem  22703  vieta1lem1  22706  vieta1lem2  22707  vieta1  22708  qaa  22719  aareccl  22722  geolim3  22735  aaliou3lem9  22746  coseq00topi  22895  cosne0  22917  tanord  22925  tanarg  23004  cxpne0  23058  cxpsqrt  23084  chordthmlem  23163  chordthmlem2  23164  dcubic  23177  mcubic  23178  cubic2  23179  cubic  23180  quartlem4  23191  atandmneg  23237  atandmcj  23240  atancj  23241  atanrecl  23242  atanlogsublem  23246  efiatan2  23248  tanatan  23250  atandmtan  23251  cosatan  23252  cosatanne0  23253  wilthlem2  23343  ftalem7  23352  basellem2  23355  basellem4  23357  basellem5  23358  isppw  23388  dchrptlem2  23540  lgsne0  23608  2sqlem8a  23646  2sqlem8  23647  tglnpt2  24021  midexlem  24069  colperpexlem3  24106  mideulem2  24108  lnopp2hpgb  24132  edgwlk  24531  wwlknext  24724  vdn0frgrav2  25023  vdgn0frgrav2  25024  vdn1frgrav2  25025  vdgn1frgrav2  25026  imadifxp  27458  nn0sqeq1  27562  xaddeq0  27573  xrge0iifhom  27919  logccne0OLD  28011  logbrec  28021  signswn0  28517  signsvtn0  28527  signstfvneq0  28529  derangenlem  28615  subfacp1lem3  28626  subfacp1lem5  28628  wsuclem  29381  nobndlem8  29459  tan2h  30047  heicant  30049  itg2addnclem2  30067  ivthALT  30153  neibastop1  30177  cmpfiiin  30629  pell1234qrne0  30789  rmxyneg  30856  bezoutr1  30924  fnwe2lem2  30997  kelac1  31009  radcnvrat  31195  binomcxplemfrat  31256  binomcxplemradcnv  31257  ioondisj2  31525  ioondisj1  31526  lptioo2  31637  lptioo1  31638  0ellimcdiv  31655  ioodvbdlimc1  31730  ioodvbdlimc2  31732  stoweidlem31  31813  stoweidlem59  31841  wallispilem4  31850  wallispi  31852  stirlinglem3  31858  stirlinglem14  31869  dirkerper  31878  dirkertrigeq  31883  dirkercncflem2  31886  fourierdlem4  31893  fourierdlem30  31919  fourierdlem41  31930  fourierdlem42  31931  fourierdlem44  31933  fourierdlem46  31935  fourierdlem48  31937  fourierdlem49  31938  fourierdlem62  31951  fourierdlem74  31963  fourierdlem75  31964  fourierdlem79  31968  fourierdlem102  31991  fourierdlem114  32003  fouriersw  32014  elaa2lem  32016  elaa2  32017  etransclem24  32041  etransclem44  32061  etransclem47  32064  lswn0  32343  el0ldep  33067  islindeps2  33084  ldepsnlinclem1  33106  ldepsnlinclem2  33107  lsatfixedN  34734  islshpat  34742  lkrshp  34830  2llnm3N  35293  dalemdnee  35390  cdleme18b  36017  cdleme40m  36193  cdlemg12g  36375  cdlemh  36543  cdlemj3  36549  tendoconid  36555  cdlemk3  36559  cdlemk12  36576  cdlemk12u  36598  cdlemk46  36674  cdlemk54  36684  erngdvlem4  36717  erngdvlem4-rN  36725  dibn0  36880  dihglblem2aN  37020  dochshpncl  37111  dochsnnz  37177  dochsatshpb  37179  lcfl7lem  37226  lcfl8b  37231  lcfrlem33  37302  lcfr  37312  hdmaprnlem3uN  37581  wnefimgd  37974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654