Theorem neeqtrd 3012

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ne 2943

This theorem is referenced by:  neeqtrrd  3017  3netr3d  3019  xaddass2  12913  xov1plusxeqvd  13159  smndex2dnrinv  18469  ablsimpgfindlem1  19625  issubdrg  19964  qsssubdrg  20569  ply1scln0  21372  alexsublem  23103  cphsubrglem  24246  cphreccllem  24247  mdegldg  25136  tglinethru  26901  footexALT  26983  footexlem2  26985  0ringprmidl  31527  nosep2o  33812  noetainflem4  33870  poimirlem26  35730  lkrpssN  37104  lnatexN  37720  lhpexle2lem  37950  lhpexle3lem  37952  cdlemg47  38677  cdlemk54  38899  tendoinvcl  39045  lcdlkreqN  39563  mapdh8ab  39718  jm2.26lem3  40739  stoweidlem36  43467