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

Theorem neeqtrrd 2743
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 2451 . 2  |-  ( ph  ->  B  =  C )
41, 3neeqtrd 2738 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    =/= wne 2638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-ne 2640
This theorem is referenced by:  3netr4d  2748  ttukeylem7  8898  znnenlem  13822  expnprm  14298  symgextf1lem  16319  isabvd  17343  flimclslem  20358  logne0  22859  chordthmlem  23035  atandmtan  23123  dchrptlem3  23413  opphllem6  23996  isusgra0  24219  usgraop  24222  signstfveq0a  28406  subfacp1lem5  28501  nodenselem3  29418  ovoliunnfl  30031  voliunnfl  30033  volsupnfl  30034  islindeps2  32819  cdleme40n  35934  cdleme40w  35936  cdlemg33c  36174  cdlemg33e  36176  trlcocnvat  36190  cdlemh2  36282  cdlemh  36283  cdlemj3  36289  cdlemk24-3  36369  cdlemkfid1N  36387  erng1r  36461  dvalveclem  36492  tendoinvcl  36571  tendolinv  36572  tendorinv  36573  dihatlat  36801  mapdpglem18  37156  mapdpglem22  37160  baerlem5amN  37183  baerlem5bmN  37184  baerlem5abmN  37185  mapdindp1  37187  mapdindp4  37190  hdmap14lem4a  37341  imo72b2lem0  37651  imo72b2lem2  37653  imo72b2lem1  37657  imo72b2  37662
  Copyright terms: Public domain W3C validator