Theorem neeqtrd 2863

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

Syntax hints:   -> wi 4   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  neeqtrrd  2868  3netr3d  2870  xaddass2  12080  xov1plusxeqvd  12318  issubdrg  18805  ply1scln0  19661  qsssubdrg  19805  alexsublem  21848  cphsubrglem  22977  cphreccllem  22978  mdegldg  23826  tglinethru  25531  footex  25613  poimirlem26  33435  lkrpssN  34450  lnatexN  35065  lhpexle2lem  35295  lhpexle3lem  35297  cdlemg47  36024  cdlemk54  36246  tendoinvcl  36393  lcdlkreqN  36911  mapdh8ab  37066  jm2.26lem3  37568  stoweidlem36  40253