Theorem neeqtrd 2762

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

Syntax hints:   -> wi 4   = wceq 1379   =/= wne 2662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664

This theorem is referenced by:  neeqtrrd  2767  3netr3d  2770  xaddass2  11438  xov1plusxeqvd  11662  issubdrg  17234  ply1scln0  18100  qsssubdrg  18242  alexsublem  20276  cphsubrglem  21356  cphreccllem  21357  mdegldg  22198  tglinethru  23727  footex  23800  eupath2lem3  24652  jm2.26lem3  30547  stoweidlem36  31336  lkrpssN  33960  lnatexN  34575  lhpexle2lem  34805  lhpexle3lem  34807  cdlemg47  35532  cdlemk54  35754  tendoinvcl  35901  lcdlkreqN  36419  mapdh8ab  36574