MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqnetrrd Structured version   Unicode version

Theorem eqnetrrd 2628
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
StepHypRef Expression
1 eqnetrrd.1 . . 3  |-  ( ph  ->  A  =  B )
21eqcomd 2448 . 2  |-  ( ph  ->  B  =  A )
3 eqnetrrd.2 . 2  |-  ( ph  ->  A  =/=  C )
42, 3eqnetrd 2626 1  |-  ( ph  ->  B  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    =/= wne 2606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436  df-ne 2608
This theorem is referenced by:  cantnflem1c  7895  cantnflem1cOLD  7918  eqsqr2d  12856  tanval2  13417  tanval3  13418  tanhlt1  13444  pcadd  13951  efgsres  16235  gsumval3OLD  16382  gsumval3  16385  ablfac  16589  isdrngrd  16858  lspsneq  17203  lebnumlem3  20535  minveclem4a  20917  evthicc  20943  ioorf  21053  deg1ldgn  21564  fta1blem  21640  vieta1lem1  21776  vieta1lem2  21777  vieta1  21778  tanregt0  21995  isosctrlem2  22217  angpieqvd  22226  chordthmlem2  22228  dcubic2  22239  dquartlem1  22246  dquart  22248  asinlem  22263  atandmcj  22304  2efiatan  22313  tanatan  22314  dvatan  22330  footex  23109  ttgcontlem1  23131  eupath2lem3  23600  bcm1n  26079  sibfof  26726  dmgmn0  27012  dmgmdivn0  27014  lgamgulmlem2  27016  gamne0  27032  heicant  28426  heiborlem6  28715  stoweidlem31  29826  stoweidlem59  29854  wallispilem4  29863  lkrlspeqN  32816  cdlemg18d  34325  cdlemg21  34330  dibord  34804  lclkrlem2u  35172  lcfrlem9  35195  mapdindp4  35368  hdmaprnlem3uN  35499  hdmaprnlem9N  35505
  Copyright terms: Public domain W3C validator