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

Theorem neeqtrrd 2762
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 2470 . 2  |-  ( ph  ->  B  =  C )
41, 3neeqtrd 2757 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374    =/= wne 2657
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-ext 2440
This theorem depends on definitions:  df-bi 185  df-cleq 2454  df-ne 2659
This theorem is referenced by:  3netr4d  2767  ttukeylem7  8886  znnenlem  13797  expnprm  14271  symgextf1lem  16235  isabvd  17247  flimclslem  20215  logne0  22710  chordthmlem  22886  atandmtan  22974  dchrptlem3  23264  isusgra0  24012  usgraop  24015  signstfveq0a  28161  subfacp1lem5  28256  nodenselem3  29008  ovoliunnfl  29622  voliunnfl  29624  volsupnfl  29625  islindeps2  32034  cdleme40n  35141  cdleme40w  35143  cdlemg33c  35381  cdlemg33e  35383  trlcocnvat  35397  cdlemh2  35489  cdlemh  35490  cdlemj3  35496  cdlemk24-3  35576  cdlemkfid1N  35594  erng1r  35668  dvalveclem  35699  tendoinvcl  35778  tendolinv  35779  tendorinv  35780  dihatlat  36008  mapdpglem18  36363  mapdpglem22  36367  baerlem5amN  36390  baerlem5bmN  36391  baerlem5abmN  36392  mapdindp1  36394  mapdindp4  36397  hdmap14lem4a  36548
  Copyright terms: Public domain W3C validator