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

Theorem neeqtrrd 2754
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 2462 . 2  |-  ( ph  ->  B  =  C )
41, 3neeqtrd 2749 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    =/= wne 2649
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446  df-ne 2651
This theorem is referenced by:  3netr4d  2759  ttukeylem7  8886  znnenlem  14029  expnprm  14505  symgextf1lem  16644  isabvd  17664  flimclslem  20651  chordthmlem  23360  atandmtan  23448  dchrptlem3  23739  opphllem6  24325  isusgra0  24549  usgraop  24552  signstfveq0a  28797  subfacp1lem5  28892  nodenselem3  29683  ovoliunnfl  30296  voliunnfl  30298  volsupnfl  30299  islindeps2  33338  cdleme40n  36591  cdleme40w  36593  cdlemg33c  36831  cdlemg33e  36833  trlcocnvat  36847  cdlemh2  36939  cdlemh  36940  cdlemj3  36946  cdlemk24-3  37026  cdlemkfid1N  37044  erng1r  37118  dvalveclem  37149  tendoinvcl  37228  tendolinv  37229  tendorinv  37230  dihatlat  37458  mapdpglem18  37813  mapdpglem22  37817  baerlem5amN  37840  baerlem5bmN  37841  baerlem5abmN  37842  mapdindp1  37844  mapdindp4  37847  hdmap14lem4a  37998  imo72b2lem0  38434  imo72b2lem2  38436  imo72b2lem1  38440  imo72b2  38445
  Copyright terms: Public domain W3C validator