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

Theorem neeqtrrd 2470
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 2288 . 2  |-  ( ph  ->  B  =  C )
41, 3neeqtrd 2468 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  ttukeylem7  8142  znnenlem  12490  expnprm  12950  isabvd  15585  flimclslem  17679  logne0  19956  ang180lem5  20111  isosctrlem3  20120  chordthmlem  20129  atandmtan  20216  dchrptlem3  20505  cntnevol  23175  subfacp1lem5  23715  nodenselem3  24337  stoweidlem23  27772  isusgra0  28106  cdleme40n  30657  cdleme40w  30659  cdlemg33c  30897  cdlemg33e  30899  trlcocnvat  30913  cdlemh2  31005  cdlemh  31006  cdlemj3  31012  cdlemk24-3  31092  cdlemkfid1N  31110  erng1r  31184  dvalveclem  31215  tendoinvcl  31294  tendolinv  31295  tendorinv  31296  dihatlat  31524  mapdpglem18  31879  mapdpglem22  31883  baerlem5amN  31906  baerlem5bmN  31907  baerlem5abmN  31908  mapdindp1  31910  mapdindp4  31913  hdmap14lem4a  32064
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-ne 2448
  Copyright terms: Public domain W3C validator