Theorem eqnetrrd 2862

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

Hypotheses

Ref	Expression
eqnetrrd.1	|- ( ph -> A = B )
eqnetrrd.2	|- ( ph -> A =/= C )

Assertion

Ref	Expression
eqnetrrd	|- ( ph -> B =/= C )

Proof of Theorem eqnetrrd

Step	Hyp	Ref	Expression
1		eqnetrrd.1	. . 3 |- ( ph -> A = B )
2	1	eqcomd 2628	. 2 |- ( ph -> B = A )
3		eqnetrrd.2	. 2 |- ( ph -> A =/= C )
4	2, 3	eqnetrd 2861	1 |- ( ph -> B =/= C )

Syntax hints:   -> wi 4   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  syl5eqner  2869  3netr3d  2870  cantnflem1c  8584  eqsqrt2d  14108  tanval2  14863  tanval3  14864  tanhlt1  14890  pcadd  15593  efgsres  18151  gsumval3  18308  ablfac  18487  isdrngrd  18773  lspsneq  19122  lebnumlem3  22762  minveclem4a  23201  evthicc  23228  ioorf  23341  deg1ldgn  23853  fta1blem  23928  vieta1lem1  24065  vieta1lem2  24066  vieta1  24067  tanregt0  24285  isosctrlem2  24549  angpieqvd  24558  chordthmlem2  24560  dcubic2  24571  dquartlem1  24578  dquart  24580  asinlem  24595  atandmcj  24636  2efiatan  24645  tanatan  24646  dvatan  24662  dmgmn0  24752  dmgmdivn0  24754  lgamgulmlem2  24756  gamne0  24772  footex  25613  ttgcontlem1  25765  wlkn0  26516  bcm1n  29554  sibfof  30402  nosep1o  31832  noetalem3  31865  finxpreclem2  33227  poimirlem9  33418  heicant  33444  heiborlem6  33615  lkrlspeqN  34458  cdlemg18d  35969  cdlemg21  35974  dibord  36448  lclkrlem2u  36816  lcfrlem9  36839  mapdindp4  37012  hdmaprnlem3uN  37143  hdmaprnlem9N  37149  binomcxplemnotnn0  38555  dstregt0  39493  stoweidlem31  40248  stoweidlem59  40276  wallispilem4  40285  dirkertrigeqlem2  40316  fourierdlem43  40367  fourierdlem65  40388