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

Theorem neeqtrrd 2625
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 2441 . 2  |-  ( ph  ->  B  =  C )
41, 3neeqtrd 2623 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    =/= wne 2599
This theorem is referenced by:  ttukeylem7  8395  znnenlem  12811  expnprm  13271  isabvd  15908  flimclslem  18016  logne0  20497  chordthmlem  20673  atandmtan  20760  dchrptlem3  21050  isusgra0  21376  subfacp1lem5  24870  nodenselem3  25638  ovoliunnfl  26248  voliunnfl  26250  volsupnfl  26251  cdleme40n  31265  cdleme40w  31267  cdlemg33c  31505  cdlemg33e  31507  trlcocnvat  31521  cdlemh2  31613  cdlemh  31614  cdlemj3  31620  cdlemk24-3  31700  cdlemkfid1N  31718  erng1r  31792  dvalveclem  31823  tendoinvcl  31902  tendolinv  31903  tendorinv  31904  dihatlat  32132  mapdpglem18  32487  mapdpglem22  32491  baerlem5amN  32514  baerlem5bmN  32515  baerlem5abmN  32516  mapdindp1  32518  mapdindp4  32521  hdmap14lem4a  32672
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429  df-ne 2601
  Copyright terms: Public domain W3C validator