Theorem neeqtrd 3010

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 3001	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐶))
4	1, 3	mpbid 232	1 ⊢ (𝜑 → 𝐴 ≠ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2940

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 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941

This theorem is referenced by:  neeqtrrd  3015  3netr3d  3017  xaddass2  13292  xov1plusxeqvd  13538  smndex2dnrinv  18928  ablsimpgfindlem1  20127  issubdrg  20781  qsssubdrg  21444  ply1scln0  22295  alexsublem  24052  cphsubrglem  25211  cphreccllem  25212  mdegldg  26105  nosep2o  27727  noetainflem4  27785  tglinethru  28644  footexALT  28726  footexlem2  28728  nrt2irr  30492  sdrgdvcl  33301  sdrginvcl  33302  0ringprmidl  33477  0ringmon1p  33583  irngnzply1lem  33740  irngnminplynz  33755  minplym1p  33756  algextdeglem4  33761  poimirlem26  37653  lkrpssN  39164  lnatexN  39781  lhpexle2lem  40011  lhpexle3lem  40013  cdlemg47  40738  cdlemk54  40960  tendoinvcl  41106  lcdlkreqN  41624  mapdh8ab  41779  aks6d1c5lem2  42139  aks6d1c7  42185  jm2.26lem3  43013  stoweidlem36  46051  addmodne  47346  p1modne  47349  m1modne  47350  minusmod5ne  47351  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx13starlem2  48028