Theorem neeqtrd 2752

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 2735	. 2 |- ( ph -> ( A =/= B <-> A =/= C ) )
4	1, 3	mpbid 210	1 |- ( ph -> A =/= C )

Syntax hints:   -> wi 4   = wceq 1395   =/= wne 2652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654

This theorem is referenced by:  neeqtrrd  2757  3netr3d  2760  xaddass2  11467  xov1plusxeqvd  11691  issubdrg  17580  ply1scln0  18458  qsssubdrg  18603  alexsublem  20669  cphsubrglem  21749  cphreccllem  21750  mdegldg  22591  tglinethru  24141  footex  24220  eupath2lem3  25105  jm2.26lem3  31105  stoweidlem36  31979  lkrpssN  34989  lnatexN  35604  lhpexle2lem  35834  lhpexle3lem  35836  cdlemg47  36563  cdlemk54  36785  tendoinvcl  36932  lcdlkreqN  37450  mapdh8ab  37605