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  13186  xov1plusxeqvd  13435  smndex2dnrinv  18824  ablsimpgfindlem1  20023  issubdrg  20700  qsssubdrg  21368  ply1scln0  22211  alexsublem  23964  cphsubrglem  25110  cphreccllem  25111  mdegldg  26004  nosep2o  27627  noetainflem4  27685  tglinethru  28616  footexALT  28698  footexlem2  28700  nrt2irr  30452  sdrgdvcl  33265  sdrginvcl  33266  0ringprmidl  33413  0ringmon1p  33519  irngnzply1lem  33678  irngnminplynz  33695  minplym1p  33696  minplynzm1p  33697  algextdeglem4  33703  poimirlem26  37633  lkrpssN  39149  lnatexN  39766  lhpexle2lem  39996  lhpexle3lem  39998  cdlemg47  40723  cdlemk54  40945  tendoinvcl  41091  lcdlkreqN  41609  mapdh8ab  41764  aks6d1c5lem2  42119  aks6d1c7  42165  jm2.26lem3  42983  stoweidlem36  46027  addmodne  47338  p1modne  47341  m1modne  47342  minusmod5ne  47343  gpg5nbgrvtx03starlem2  48053  gpg5nbgrvtx13starlem2  48056