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

Theorem eqnetrrd 2748
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 2462 . 2  |-  ( ph  ->  B  =  A )
3 eqnetrrd.2 . 2  |-  ( ph  ->  A  =/=  C )
42, 3eqnetrd 2747 1  |-  ( ph  ->  B  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    =/= wne 2649
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446  df-ne 2651
This theorem is referenced by:  syl5eqner  2755  3netr3d  2757  cantnflem1c  8097  cantnflem1cOLD  8120  eqsqrt2d  13283  tanval2  13950  tanval3  13951  tanhlt1  13977  pcadd  14492  efgsres  16955  gsumval3OLD  17107  gsumval3  17110  ablfac  17334  isdrngrd  17617  lspsneq  17963  lebnumlem3  21629  minveclem4a  22011  evthicc  22037  ioorf  22148  deg1ldgn  22659  fta1blem  22735  vieta1lem1  22872  vieta1lem2  22873  vieta1  22874  tanregt0  23092  isosctrlem2  23350  angpieqvd  23359  chordthmlem2  23361  dcubic2  23372  dquartlem1  23379  dquart  23381  asinlem  23396  atandmcj  23437  2efiatan  23446  tanatan  23447  dvatan  23463  footex  24296  ttgcontlem1  24390  eupath2lem3  25181  bcm1n  27834  sibfof  28546  dmgmn0  28832  dmgmdivn0  28834  lgamgulmlem2  28836  gamne0  28852  heicant  30289  heiborlem6  30552  binomcxplemnotnn0  31502  dstregt0  31703  stoweidlem31  32052  stoweidlem59  32080  wallispilem4  32089  dirkertrigeqlem2  32120  fourierdlem43  32171  fourierdlem65  32193  lkrlspeqN  35293  cdlemg18d  36804  cdlemg21  36809  dibord  37283  lclkrlem2u  37651  lcfrlem9  37674  mapdindp4  37847  hdmaprnlem3uN  37978  hdmaprnlem9N  37984
  Copyright terms: Public domain W3C validator