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

Theorem neeqtrrd 2748
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 2459 . 2  |-  ( ph  ->  B  =  C )
41, 3neeqtrd 2743 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    =/= wne 2644
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-cleq 2443  df-ne 2646
This theorem is referenced by:  3netr4d  2753  ttukeylem7  8787  znnenlem  13598  expnprm  14068  symgextf1lem  16029  isabvd  17013  flimclslem  19675  logne0  22169  chordthmlem  22345  atandmtan  22433  dchrptlem3  22723  isusgra0  23412  signstfveq0a  27113  subfacp1lem5  27208  nodenselem3  27960  ovoliunnfl  28573  voliunnfl  28575  volsupnfl  28576  islindeps2  31126  cdleme40n  34420  cdleme40w  34422  cdlemg33c  34660  cdlemg33e  34662  trlcocnvat  34676  cdlemh2  34768  cdlemh  34769  cdlemj3  34775  cdlemk24-3  34855  cdlemkfid1N  34873  erng1r  34947  dvalveclem  34978  tendoinvcl  35057  tendolinv  35058  tendorinv  35059  dihatlat  35287  mapdpglem18  35642  mapdpglem22  35646  baerlem5amN  35669  baerlem5bmN  35670  baerlem5abmN  35671  mapdindp1  35673  mapdindp4  35676  hdmap14lem4a  35827
  Copyright terms: Public domain W3C validator