Theorem neeqtrd 2994

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  neeqtrrd  2999  3netr3d  3001  xaddass2  13152  xov1plusxeqvd  13401  smndex2dnrinv  18789  ablsimpgfindlem1  19988  issubdrg  20665  qsssubdrg  21333  ply1scln0  22176  alexsublem  23929  cphsubrglem  25075  cphreccllem  25076  mdegldg  25969  nosep2o  27592  noetainflem4  27650  tglinethru  28581  footexALT  28663  footexlem2  28665  nrt2irr  30417  sdrgdvcl  33239  sdrginvcl  33240  0ringprmidl  33387  0ringmon1p  33493  irngnzply1lem  33663  irngnminplynz  33685  minplym1p  33686  minplynzm1p  33687  algextdeglem4  33693  poimirlem26  37636  lkrpssN  39152  lnatexN  39768  lhpexle2lem  39998  lhpexle3lem  40000  cdlemg47  40725  cdlemk54  40947  tendoinvcl  41093  lcdlkreqN  41611  mapdh8ab  41766  aks6d1c5lem2  42121  aks6d1c7  42167  jm2.26lem3  42984  stoweidlem36  46027  addmodne  47338  p1modne  47341  m1modne  47342  minusmod5ne  47343  gpg5nbgrvtx03starlem2  48063  gpg5nbgrvtx13starlem2  48066  gpg5edgnedg  48124