Theorem neeqtrd 2693

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

Syntax hints:   -> wi 4   = wceq 1444   =/= wne 2622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-cleq 2444  df-ne 2624

This theorem is referenced by:  neeqtrrd  2698  3netr3d  2700  xaddass2  11536  xov1plusxeqvd  11778  issubdrg  18033  ply1scln0  18884  qsssubdrg  19027  alexsublem  21059  cphsubrglem  22155  cphreccllem  22156  mdegldg  23015  tglinethru  24681  footex  24763  eupath2lem3  25707  poimirlem26  31966  lkrpssN  32729  lnatexN  33344  lhpexle2lem  33574  lhpexle3lem  33576  cdlemg47  34303  cdlemk54  34525  tendoinvcl  34672  lcdlkreqN  35190  mapdh8ab  35345  jm2.26lem3  35856  stoweidlem36  37897