Theorem neeqtrd 3007

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

Syntax hints:   → wi 4   = wceq 1536   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ne 2938

This theorem is referenced by:  neeqtrrd  3012  3netr3d  3014  xaddass2  13288  xov1plusxeqvd  13534  smndex2dnrinv  18940  ablsimpgfindlem1  20141  issubdrg  20797  qsssubdrg  21461  ply1scln0  22310  alexsublem  24067  cphsubrglem  25224  cphreccllem  25225  mdegldg  26119  nosep2o  27741  noetainflem4  27799  tglinethru  28658  footexALT  28740  footexlem2  28742  nrt2irr  30501  sdrgdvcl  33280  sdrginvcl  33281  0ringprmidl  33456  0ringmon1p  33562  irngnzply1lem  33704  irngnminplynz  33719  minplym1p  33720  algextdeglem4  33725  poimirlem26  37632  lkrpssN  39144  lnatexN  39761  lhpexle2lem  39991  lhpexle3lem  39993  cdlemg47  40718  cdlemk54  40940  tendoinvcl  41086  lcdlkreqN  41604  mapdh8ab  41759  aks6d1c5lem2  42119  aks6d1c7  42165  jm2.26lem3  42989  stoweidlem36  45991  addmodne  47283  p1modne  47286  m1modne  47287  minusmod5ne  47288  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx13starlem2  47962