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

Theorem neeqtrrd 2717
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 2477 . 2  |-  ( ph  ->  B  =  C )
41, 3neeqtrd 2712 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1452    =/= wne 2641
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-cleq 2464  df-ne 2643
This theorem is referenced by:  3netr4d  2720  ttukeylem7  8963  modsumfzodifsn  12196  znnenlem  14341  expnprm  14926  symgextf1lem  17139  isabvd  18126  flimclslem  21077  chordthmlem  23837  atandmtan  23925  dchrptlem3  24273  opphllem6  24873  isusgra0  25153  usgraop  25156  signstfveq0a  29537  subfacp1lem5  29979  nodenselem3  30643  ovoliunnfl  32046  voliunnfl  32048  volsupnfl  32049  cdleme40n  34106  cdleme40w  34108  cdlemg33c  34346  cdlemg33e  34348  trlcocnvat  34362  cdlemh2  34454  cdlemh  34455  cdlemj3  34461  cdlemk24-3  34541  cdlemkfid1N  34559  erng1r  34633  dvalveclem  34664  tendoinvcl  34743  tendolinv  34744  tendorinv  34745  dihatlat  34973  mapdpglem18  35328  mapdpglem22  35332  baerlem5amN  35355  baerlem5bmN  35356  baerlem5abmN  35357  mapdindp1  35359  mapdindp4  35362  hdmap14lem4a  35513  imo72b2lem0  36679  imo72b2lem2  36681  imo72b2lem1  36685  imo72b2  36689  islindeps2  40784
  Copyright terms: Public domain W3C validator