Theorem neeqtrd 3020

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

Syntax hints:   → wi 4   = wceq 1538   ≠ wne 2951

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750  df-ne 2952

This theorem is referenced by:  neeqtrrd  3025  3netr3d  3027  xaddass2  12697  xov1plusxeqvd  12943  smndex2dnrinv  18159  ablsimpgfindlem1  19310  issubdrg  19641  qsssubdrg  20238  ply1scln0  21028  alexsublem  22757  cphsubrglem  23891  cphreccllem  23892  mdegldg  24779  tglinethru  26542  footexALT  26624  footexlem2  26626  0ringprmidl  31158  nosep2o  33482  noetainflem4  33540  poimirlem26  35397  lkrpssN  36773  lnatexN  37389  lhpexle2lem  37619  lhpexle3lem  37621  cdlemg47  38346  cdlemk54  38568  tendoinvcl  38714  lcdlkreqN  39232  mapdh8ab  39387  jm2.26lem3  40350  stoweidlem36  43079