Theorem eqnetrrd 2751

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

Hypotheses

Ref	Expression
eqnetrrd.1
eqnetrrd.2

Assertion

Ref	Expression
eqnetrrd

Proof of Theorem eqnetrrd

Step	Hyp	Ref	Expression
1		eqnetrrd.1	. . 3
2	1	eqcomd 2465	. 2
3		eqnetrrd.2	. 2
4	2, 3	eqnetrd 2750	1

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

This theorem is referenced by:  syl5eqner  2758  3netr3d  2760  cantnflem1c  8127  cantnflem1cOLD  8150  eqsqrt2d  13201  tanval2  13868  tanval3  13869  tanhlt1  13895  pcadd  14408  efgsres  16756  gsumval3OLD  16908  gsumval3  16911  ablfac  17139  isdrngrd  17422  lspsneq  17768  lebnumlem3  21463  minveclem4a  21845  evthicc  21871  ioorf  21982  deg1ldgn  22493  fta1blem  22569  vieta1lem1  22706  vieta1lem2  22707  vieta1  22708  tanregt0  22926  isosctrlem2  23153  angpieqvd  23162  chordthmlem2  23164  dcubic2  23175  dquartlem1  23182  dquart  23184  asinlem  23199  atandmcj  23240  2efiatan  23249  tanatan  23250  dvatan  23266  footex  24095  ttgcontlem1  24188  eupath2lem3  24979  bcm1n  27600  sibfof  28282  dmgmn0  28568  dmgmdivn0  28570  lgamgulmlem2  28572  gamne0  28588  heicant  30049  heiborlem6  30312  binomcxplemnotnn0  31261  dstregt0  31463  stoweidlem31  31813  stoweidlem59  31841  wallispilem4  31850  dirkertrigeqlem2  31881  fourierdlem43  31932  fourierdlem65  31954  lkrlspeqN  34896  cdlemg18d  36407  cdlemg21  36412  dibord  36886  lclkrlem2u  37254  lcfrlem9  37277  mapdindp4  37450  hdmaprnlem3uN  37581  hdmaprnlem9N  37587

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