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 1540   ≠ wne 2932

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  neeqtrrd  3006  3netr3d  3008  xaddass2  13266  xov1plusxeqvd  13515  smndex2dnrinv  18893  ablsimpgfindlem1  20090  issubdrg  20740  qsssubdrg  21394  ply1scln0  22229  alexsublem  23982  cphsubrglem  25129  cphreccllem  25130  mdegldg  26023  nosep2o  27646  noetainflem4  27704  tglinethru  28615  footexALT  28697  footexlem2  28699  nrt2irr  30454  sdrgdvcl  33293  sdrginvcl  33294  0ringprmidl  33464  0ringmon1p  33570  irngnzply1lem  33731  irngnminplynz  33746  minplym1p  33747  minplynzm1p  33748  algextdeglem4  33754  poimirlem26  37670  lkrpssN  39181  lnatexN  39798  lhpexle2lem  40028  lhpexle3lem  40030  cdlemg47  40755  cdlemk54  40977  tendoinvcl  41123  lcdlkreqN  41641  mapdh8ab  41796  aks6d1c5lem2  42151  aks6d1c7  42197  jm2.26lem3  43025  stoweidlem36  46065  addmodne  47373  p1modne  47376  m1modne  47377  minusmod5ne  47378  gpg5nbgrvtx03starlem2  48071  gpg5nbgrvtx13starlem2  48074