Theorem neeqtrd 3009

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-ne 2940

This theorem is referenced by:  neeqtrrd  3014  3netr3d  3016  xaddass2  13179  xov1plusxeqvd  13425  smndex2dnrinv  18739  ablsimpgfindlem1  19900  issubdrg  20296  qsssubdrg  20893  ply1scln0  21699  alexsublem  23432  cphsubrglem  24578  cphreccllem  24579  mdegldg  25468  nosep2o  27067  noetainflem4  27125  tglinethru  27641  footexALT  27723  footexlem2  27725  sdrgdvcl  32145  sdrginvcl  32146  0ringprmidl  32298  0ringmon1p  32340  irngnzply1lem  32451  poimirlem26  36177  lkrpssN  37698  lnatexN  38315  lhpexle2lem  38545  lhpexle3lem  38547  cdlemg47  39272  cdlemk54  39494  tendoinvcl  39640  lcdlkreqN  40158  mapdh8ab  40313  jm2.26lem3  41383  stoweidlem36  44397