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

Theorem eqnetrrd 2499
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 2321 . 2  |-  ( ph  ->  B  =  A )
3 eqnetrrd.2 . 2  |-  ( ph  ->  A  =/=  C )
42, 3eqnetrd 2497 1  |-  ( ph  ->  B  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1633    =/= wne 2479
This theorem is referenced by:  cantnflem1c  7434  eqsqr2d  11899  tanval2  12460  tanval3  12461  tanhlt1  12487  pcadd  12984  efgsres  15096  gsumval3  15240  ablfac  15372  isdrngrd  15587  lspsneq  15924  lebnumlem3  18514  minveclem4a  18847  evthicc  18872  ioorf  18981  deg1ldgn  19532  fta1blem  19607  vieta1lem1  19743  vieta1lem2  19744  vieta1  19745  tanregt0  19954  isosctrlem2  20172  angpieqvd  20181  chordthmlem2  20183  dcubic2  20193  dquartlem1  20200  dquart  20202  asinlem  20217  atandmcj  20258  2efiatan  20267  tanatan  20268  dvatan  20284  bcm1n  23298  eupath2lem3  24187  heiborlem6  25688  stoweidlem31  26928  wallispilem4  26965  lkrlspeqN  29179  cdlemg18d  30688  cdlemg21  30693  dibord  31167  lclkrlem2u  31535  lcfrlem9  31558  mapdindp4  31731  hdmaprnlem3uN  31862  hdmaprnlem9N  31868
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-11 1732  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-ex 1533  df-cleq 2309  df-ne 2481
  Copyright terms: Public domain W3C validator