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

Theorem neeqtrrd 2483
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
Hypotheses
Ref Expression
neeqtrrd.1  |-  ( ph  ->  A  =/=  B )
neeqtrrd.2  |-  ( ph  ->  C  =  B )
Assertion
Ref Expression
neeqtrrd  |-  ( ph  ->  A  =/=  C )

Proof of Theorem neeqtrrd
StepHypRef Expression
1 neeqtrrd.1 . 2  |-  ( ph  ->  A  =/=  B )
2 neeqtrrd.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2301 . 2  |-  ( ph  ->  B  =  C )
41, 3neeqtrd 2481 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  ttukeylem7  8158  znnenlem  12506  expnprm  12966  isabvd  15601  flimclslem  17695  logne0  19972  ang180lem5  20127  isosctrlem3  20136  chordthmlem  20145  atandmtan  20232  dchrptlem3  20521  cntnevol  23191  subfacp1lem5  23730  nodenselem3  24408  ovoliunnfl  25001  stoweidlem23  27875  isusgra0  28238  cdleme40n  31279  cdleme40w  31281  cdlemg33c  31519  cdlemg33e  31521  trlcocnvat  31535  cdlemh2  31627  cdlemh  31628  cdlemj3  31634  cdlemk24-3  31714  cdlemkfid1N  31732  erng1r  31806  dvalveclem  31837  tendoinvcl  31916  tendolinv  31917  tendorinv  31918  dihatlat  32146  mapdpglem18  32501  mapdpglem22  32505  baerlem5amN  32528  baerlem5bmN  32529  baerlem5abmN  32530  mapdindp1  32532  mapdindp4  32535  hdmap14lem4a  32686
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-ne 2461
  Copyright terms: Public domain W3C validator