Theorem neeqtrd 2747

Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)

Hypotheses

Ref	Expression
neeqtrd.1	|- ( ph -> A =/= B )
neeqtrd.2	|- ( ph -> B = C )

Assertion

Ref	Expression
neeqtrd	|- ( ph -> A =/= C )

Proof of Theorem neeqtrd

Step	Hyp	Ref	Expression
1		neeqtrd.1	. 2 |- ( ph -> A =/= B )
2		neeqtrd.2	. . 3 |- ( ph -> B = C )
3	2	neeq2d 2730	. 2 |- ( ph -> ( A =/= B <-> A =/= C ) )
4	1, 3	mpbid 210	1 |- ( ph -> A =/= C )

Syntax hints:   -> wi 4   = wceq 1370   =/= wne 2648

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 2432

This theorem depends on definitions:  df-bi 185  df-cleq 2446  df-ne 2650

This theorem is referenced by:  neeqtrrd  2752  3netr3d  2755  xaddass2  11325  xov1plusxeqvd  11549  issubdrg  17014  ply1scln0  17869  qsssubdrg  17998  alexsublem  19749  cphsubrglem  20829  cphreccllem  20830  mdegldg  21671  tglinethru  23182  footex  23255  eupath2lem3  23753  jm2.26lem3  29499  stoweidlem36  29980  lkrpssN  33147  lnatexN  33762  lhpexle2lem  33992  lhpexle3lem  33994  cdlemg47  34719  cdlemk54  34941  tendoinvcl  35088  lcdlkreqN  35606  mapdh8ab  35761