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 222	1 ⊢ (𝜑 → 𝐴 ≠ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-ne 2944

This theorem is referenced by:  neeqtrrd  3017  3netr3d  3019  xaddass2  12285  xov1plusxeqvd  12525  issubdrg  19015  ply1scln0  19876  qsssubdrg  20020  alexsublem  22068  cphsubrglem  23196  cphreccllem  23197  mdegldg  24046  tglinethru  25752  footex  25834  poimirlem26  33768  lkrpssN  34972  lnatexN  35588  lhpexle2lem  35818  lhpexle3lem  35820  cdlemg47  36546  cdlemk54  36768  tendoinvcl  36914  lcdlkreqN  37432  mapdh8ab  37587  jm2.26lem3  38094  stoweidlem36  40767