Theorem neeqtrd 3085

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

Syntax hints:   → wi 4   = wceq 1533   ≠ wne 3016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-ne 3017

This theorem is referenced by:  neeqtrrd  3090  3netr3d  3092  xaddass2  12642  xov1plusxeqvd  12883  smndex2dnrinv  18079  ablsimpgfindlem1  19228  issubdrg  19559  ply1scln0  20458  qsssubdrg  20603  alexsublem  22651  cphsubrglem  23780  cphreccllem  23781  mdegldg  24659  tglinethru  26421  footexALT  26503  footexlem2  26505  poimirlem26  34917  lkrpssN  36298  lnatexN  36914  lhpexle2lem  37144  lhpexle3lem  37146  cdlemg47  37871  cdlemk54  38093  tendoinvcl  38239  lcdlkreqN  38757  mapdh8ab  38912  jm2.26lem3  39596  stoweidlem36  42320