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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  neeqtrrd  3006  3netr3d  3008  xaddass2  13202  xov1plusxeqvd  13451  smndex2dnrinv  18886  ablsimpgfindlem1  20084  issubdrg  20757  qsssubdrg  21406  ply1scln0  22256  alexsublem  24009  cphsubrglem  25144  cphreccllem  25145  mdegldg  26031  nosep2o  27646  noetainflem4  27704  tglinethru  28704  footexALT  28786  footexlem2  28788  nrt2irr  30543  sdrgdvcl  33360  sdrginvcl  33361  0ringprmidl  33509  0ringmon1p  33617  irngnzply1lem  33834  irngnminplynz  33856  minplym1p  33857  minplynzm1p  33858  algextdeglem4  33864  mh-inf3f1  36723  poimirlem26  37967  lkrpssN  39609  lnatexN  40225  lhpexle2lem  40455  lhpexle3lem  40457  cdlemg47  41182  cdlemk54  41404  tendoinvcl  41550  lcdlkreqN  42068  mapdh8ab  42223  aks6d1c5lem2  42577  aks6d1c7  42623  jm2.26lem3  43429  stoweidlem36  46464  addmodne  47798  p1modne  47801  m1modne  47802  minusmod5ne  47803  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx13starlem2  48548  gpg5edgnedg  48606