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

Theorem eqnetrrd 2626
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 2446 . 2  |-  ( ph  ->  B  =  A )
3 eqnetrrd.2 . 2  |-  ( ph  ->  A  =/=  C )
42, 3eqnetrd 2624 1  |-  ( ph  ->  B  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364    =/= wne 2604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-ex 1592  df-cleq 2434  df-ne 2606
This theorem is referenced by:  cantnflem1c  7891  cantnflem1cOLD  7914  eqsqr2d  12852  tanval2  13413  tanval3  13414  tanhlt1  13440  pcadd  13947  efgsres  16228  gsumval3OLD  16375  gsumval3  16378  ablfac  16579  isdrngrd  16838  lspsneq  17181  lebnumlem3  20435  minveclem4a  20817  evthicc  20843  ioorf  20953  deg1ldgn  21507  fta1blem  21583  vieta1lem1  21719  vieta1lem2  21720  vieta1  21721  tanregt0  21938  isosctrlem2  22160  angpieqvd  22169  chordthmlem2  22171  dcubic2  22182  dquartlem1  22189  dquart  22191  asinlem  22206  atandmcj  22247  2efiatan  22256  tanatan  22257  dvatan  22273  ttgcontlem1  23050  eupath2lem3  23519  bcm1n  25996  sibfof  26640  dmgmn0  26926  dmgmdivn0  26928  lgamgulmlem2  26930  gamne0  26946  heicant  28335  heiborlem6  28624  stoweidlem31  29735  stoweidlem59  29763  wallispilem4  29772  lkrlspeqN  32504  cdlemg18d  34013  cdlemg21  34018  dibord  34492  lclkrlem2u  34860  lcfrlem9  34883  mapdindp4  35056  hdmaprnlem3uN  35187  hdmaprnlem9N  35193
  Copyright terms: Public domain W3C validator