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

Theorem eqnetrrd 2761
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 2475 . 2  |-  ( ph  ->  B  =  A )
3 eqnetrrd.2 . 2  |-  ( ph  ->  A  =/=  C )
42, 3eqnetrd 2760 1  |-  ( ph  ->  B  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    =/= wne 2662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664
This theorem is referenced by:  syl5eqner  2768  3netr3d  2770  cantnflem1c  8106  cantnflem1cOLD  8129  eqsqrt2d  13164  tanval2  13729  tanval3  13730  tanhlt1  13756  pcadd  14267  efgsres  16562  gsumval3OLD  16711  gsumval3  16714  ablfac  16941  isdrngrd  17222  lspsneq  17568  lebnumlem3  21226  minveclem4a  21608  evthicc  21634  ioorf  21745  deg1ldgn  22256  fta1blem  22332  vieta1lem1  22468  vieta1lem2  22469  vieta1  22470  tanregt0  22687  isosctrlem2  22909  angpieqvd  22918  chordthmlem2  22920  dcubic2  22931  dquartlem1  22938  dquart  22940  asinlem  22955  atandmcj  22996  2efiatan  23005  tanatan  23006  dvatan  23022  footex  23831  ttgcontlem1  23892  eupath2lem3  24683  bcm1n  27296  sibfof  27950  dmgmn0  28236  dmgmdivn0  28238  lgamgulmlem2  28240  gamne0  28256  heicant  29654  heiborlem6  29943  dstregt0  31068  stoweidlem31  31359  stoweidlem59  31387  wallispilem4  31396  dirkertrigeqlem2  31427  lkrlspeqN  33986  cdlemg18d  35495  cdlemg21  35500  dibord  35974  lclkrlem2u  36342  lcfrlem9  36365  mapdindp4  36538  hdmaprnlem3uN  36669  hdmaprnlem9N  36675
  Copyright terms: Public domain W3C validator