Theorem neeqtrd 2999

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

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

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 2706

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

This theorem is referenced by:  neeqtrrd  3004  3netr3d  3006  xaddass2  13163  xov1plusxeqvd  13412  smndex2dnrinv  18838  ablsimpgfindlem1  20036  issubdrg  20711  qsssubdrg  21379  ply1scln0  22232  alexsublem  23986  cphsubrglem  25131  cphreccllem  25132  mdegldg  26025  nosep2o  27648  noetainflem4  27706  tglinethru  28657  footexALT  28739  footexlem2  28741  nrt2irr  30497  sdrgdvcl  33330  sdrginvcl  33331  0ringprmidl  33479  0ringmon1p  33587  irngnzply1lem  33796  irngnminplynz  33818  minplym1p  33819  minplynzm1p  33820  algextdeglem4  33826  poimirlem26  37786  lkrpssN  39362  lnatexN  39978  lhpexle2lem  40208  lhpexle3lem  40210  cdlemg47  40935  cdlemk54  41157  tendoinvcl  41303  lcdlkreqN  41821  mapdh8ab  41976  aks6d1c5lem2  42331  aks6d1c7  42377  jm2.26lem3  43185  stoweidlem36  46222  addmodne  47532  p1modne  47535  m1modne  47536  minusmod5ne  47537  gpg5nbgrvtx03starlem2  48257  gpg5nbgrvtx13starlem2  48260  gpg5edgnedg  48318