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

Theorem eqnetrrd 2587
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 2409 . 2  |-  ( ph  ->  B  =  A )
3 eqnetrrd.2 . 2  |-  ( ph  ->  A  =/=  C )
42, 3eqnetrd 2585 1  |-  ( ph  ->  B  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    =/= wne 2567
This theorem is referenced by:  cantnflem1c  7599  eqsqr2d  12127  tanval2  12689  tanval3  12690  tanhlt1  12716  pcadd  13213  efgsres  15325  gsumval3  15469  ablfac  15601  isdrngrd  15816  lspsneq  16149  lebnumlem3  18941  minveclem4a  19284  evthicc  19309  ioorf  19418  deg1ldgn  19969  fta1blem  20044  vieta1lem1  20180  vieta1lem2  20181  vieta1  20182  tanregt0  20394  isosctrlem2  20616  angpieqvd  20625  chordthmlem2  20627  dcubic2  20637  dquartlem1  20644  dquart  20646  asinlem  20661  atandmcj  20702  2efiatan  20711  tanatan  20712  dvatan  20728  eupath2lem3  21654  bcm1n  24104  sibfof  24607  dmgmn0  24763  dmgmdivn0  24765  lgamgulmlem2  24767  gamne0  24783  heiborlem6  26415  stoweidlem31  27647  stoweidlem59  27675  wallispilem4  27684  lkrlspeqN  29654  cdlemg18d  31163  cdlemg21  31168  dibord  31642  lclkrlem2u  32010  lcfrlem9  32033  mapdindp4  32206  hdmaprnlem3uN  32337  hdmaprnlem9N  32343
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397  df-ne 2569
  Copyright terms: Public domain W3C validator