Theorem neeqtrd 3016

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

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  neeqtrrd  3021  3netr3d  3023  xaddass2  13312  xov1plusxeqvd  13558  smndex2dnrinv  18950  ablsimpgfindlem1  20151  issubdrg  20803  qsssubdrg  21467  ply1scln0  22316  alexsublem  24073  cphsubrglem  25230  cphreccllem  25231  mdegldg  26125  nosep2o  27745  noetainflem4  27803  tglinethru  28662  footexALT  28744  footexlem2  28746  nrt2irr  30505  sdrgdvcl  33266  sdrginvcl  33267  0ringprmidl  33442  0ringmon1p  33548  irngnzply1lem  33690  irngnminplynz  33705  minplym1p  33706  algextdeglem4  33711  poimirlem26  37606  lkrpssN  39119  lnatexN  39736  lhpexle2lem  39966  lhpexle3lem  39968  cdlemg47  40693  cdlemk54  40915  tendoinvcl  41061  lcdlkreqN  41579  mapdh8ab  41734  aks6d1c5lem2  42095  aks6d1c7  42141  jm2.26lem3  42958  stoweidlem36  45957