Theorem neeqtrd 3013

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

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ne 2944

This theorem is referenced by:  neeqtrrd  3018  3netr3d  3020  xaddass2  12984  xov1plusxeqvd  13230  smndex2dnrinv  18554  ablsimpgfindlem1  19710  issubdrg  20049  qsssubdrg  20657  ply1scln0  21462  alexsublem  23195  cphsubrglem  24341  cphreccllem  24342  mdegldg  25231  tglinethru  26997  footexALT  27079  footexlem2  27081  0ringprmidl  31625  nosep2o  33885  noetainflem4  33943  poimirlem26  35803  lkrpssN  37177  lnatexN  37793  lhpexle2lem  38023  lhpexle3lem  38025  cdlemg47  38750  cdlemk54  38972  tendoinvcl  39118  lcdlkreqN  39636  mapdh8ab  39791  jm2.26lem3  40823  stoweidlem36  43577