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

Theorem eqnetrrd 2466
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 2288 . 2  |-  ( ph  ->  B  =  A )
3 eqnetrrd.2 . 2  |-  ( ph  ->  A  =/=  C )
42, 3eqnetrd 2464 1  |-  ( ph  ->  B  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  cantnflem1c  7389  eqsqr2d  11852  tanval2  12413  tanval3  12414  tanhlt1  12440  pcadd  12937  efgsres  15047  gsumval3  15191  ablfac  15323  isdrngrd  15538  lspsneq  15875  lebnumlem3  18461  minveclem4a  18794  evthicc  18819  ioorf  18928  deg1ldgn  19479  fta1blem  19554  vieta1lem1  19690  vieta1lem2  19691  vieta1  19692  tanregt0  19901  isosctrlem2  20119  angpieqvd  20128  chordthmlem2  20130  dcubic2  20140  dquartlem1  20147  dquart  20149  asinlem  20164  atandmcj  20205  2efiatan  20214  tanatan  20215  dvatan  20231  bcm1n  23032  eupath2lem3  23903  heiborlem6  26540  stoweidlem31  27780  wallispilem4  27817  lkrlspeqN  29361  cdlemg18d  30870  cdlemg21  30875  dibord  31349  lclkrlem2u  31717  lcfrlem9  31740  mapdindp4  31913  hdmaprnlem3uN  32044  hdmaprnlem9N  32050
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-ne 2448
  Copyright terms: Public domain W3C validator