Theorem neeqtrd 3001

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ne 2933

This theorem is referenced by:  neeqtrrd  3006  3netr3d  3008  xaddass2  13167  xov1plusxeqvd  13416  smndex2dnrinv  18842  ablsimpgfindlem1  20040  issubdrg  20715  qsssubdrg  21383  ply1scln0  22236  alexsublem  23990  cphsubrglem  25135  cphreccllem  25136  mdegldg  26029  nosep2o  27652  noetainflem4  27710  tglinethru  28710  footexALT  28792  footexlem2  28794  nrt2irr  30550  sdrgdvcl  33383  sdrginvcl  33384  0ringprmidl  33532  0ringmon1p  33640  irngnzply1lem  33849  irngnminplynz  33871  minplym1p  33872  minplynzm1p  33873  algextdeglem4  33879  poimirlem26  37849  lkrpssN  39445  lnatexN  40061  lhpexle2lem  40291  lhpexle3lem  40293  cdlemg47  41018  cdlemk54  41240  tendoinvcl  41386  lcdlkreqN  41904  mapdh8ab  42059  aks6d1c5lem2  42414  aks6d1c7  42460  jm2.26lem3  43264  stoweidlem36  46301  addmodne  47611  p1modne  47614  m1modne  47615  minusmod5ne  47616  gpg5nbgrvtx03starlem2  48336  gpg5nbgrvtx13starlem2  48339  gpg5edgnedg  48397