Theorem neeqtrd 3008

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

Hypotheses

Ref	Expression
neeqtrd.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)
neeqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
neeqtrd	⊢ (𝜑 → 𝐴 ≠ 𝐶)

Proof of Theorem neeqtrd

Step	Hyp	Ref	Expression
1		neeqtrd.1	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
2		neeqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	neeq2d 2999	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐶))
4	1, 3	mpbid 231	1 ⊢ (𝜑 → 𝐴 ≠ 𝐶)

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-ne 2939

This theorem is referenced by:  neeqtrrd  3013  3netr3d  3015  xaddass2  13233  xov1plusxeqvd  13479  smndex2dnrinv  18832  ablsimpgfindlem1  20018  issubdrg  20544  qsssubdrg  21204  ply1scln0  22034  alexsublem  23768  cphsubrglem  24925  cphreccllem  24926  mdegldg  25819  nosep2o  27421  noetainflem4  27479  tglinethru  28154  footexALT  28236  footexlem2  28238  nrt2irr  29993  sdrgdvcl  32667  sdrginvcl  32668  0ringprmidl  32842  0ringmon1p  32910  irngnzply1lem  33043  irngnminplynz  33060  minplym1p  33061  algextdeglem4  33065  poimirlem26  36817  lkrpssN  38336  lnatexN  38953  lhpexle2lem  39183  lhpexle3lem  39185  cdlemg47  39910  cdlemk54  40132  tendoinvcl  40278  lcdlkreqN  40796  mapdh8ab  40951  jm2.26lem3  42042  stoweidlem36  45050