Theorem neeqtrd 3000

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-ne 2931

This theorem is referenced by:  neeqtrrd  3005  3netr3d  3007  xaddass2  13283  xov1plusxeqvd  13529  smndex2dnrinv  18905  ablsimpgfindlem1  20107  issubdrg  20759  qsssubdrg  21423  ply1scln0  22283  alexsublem  24039  cphsubrglem  25196  cphreccllem  25197  mdegldg  26093  nosep2o  27712  noetainflem4  27770  tglinethru  28563  footexALT  28645  footexlem2  28647  nrt2irr  30406  sdrgdvcl  33149  sdrginvcl  33150  0ringprmidl  33324  0ringmon1p  33430  irngnzply1lem  33566  irngnminplynz  33581  minplym1p  33582  algextdeglem4  33587  poimirlem26  37347  lkrpssN  38861  lnatexN  39478  lhpexle2lem  39708  lhpexle3lem  39710  cdlemg47  40435  cdlemk54  40657  tendoinvcl  40803  lcdlkreqN  41321  mapdh8ab  41476  aks6d1c5lem2  41836  aks6d1c7  41882  jm2.26lem3  42659  stoweidlem36  45657