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

Theorem eqnetrrd 2621
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 2441 . 2  |-  ( ph  ->  B  =  A )
3 eqnetrrd.2 . 2  |-  ( ph  ->  A  =/=  C )
42, 3eqnetrd 2619 1  |-  ( ph  ->  B  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    =/= wne 2599
This theorem is referenced by:  cantnflem1c  7643  eqsqr2d  12172  tanval2  12734  tanval3  12735  tanhlt1  12761  pcadd  13258  efgsres  15370  gsumval3  15514  ablfac  15646  isdrngrd  15861  lspsneq  16194  lebnumlem3  18988  minveclem4a  19331  evthicc  19356  ioorf  19465  deg1ldgn  20016  fta1blem  20091  vieta1lem1  20227  vieta1lem2  20228  vieta1  20229  tanregt0  20441  isosctrlem2  20663  angpieqvd  20672  chordthmlem2  20674  dcubic2  20684  dquartlem1  20691  dquart  20693  asinlem  20708  atandmcj  20749  2efiatan  20758  tanatan  20759  dvatan  20775  eupath2lem3  21701  bcm1n  24151  sibfof  24654  dmgmn0  24810  dmgmdivn0  24812  lgamgulmlem2  24814  gamne0  24830  heiborlem6  26525  stoweidlem31  27756  stoweidlem59  27784  wallispilem4  27793  lkrlspeqN  29969  cdlemg18d  31478  cdlemg21  31483  dibord  31957  lclkrlem2u  32325  lcfrlem9  32348  mapdindp4  32521  hdmaprnlem3uN  32652  hdmaprnlem9N  32658
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429  df-ne 2601
  Copyright terms: Public domain W3C validator