Theorem neeqtrd 3055

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

Syntax hints:   → wi 4   = wceq 1525   ≠ wne 2986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-cleq 2790  df-ne 2987

This theorem is referenced by:  neeqtrrd  3060  3netr3d  3062  xaddass2  12497  xov1plusxeqvd  12738  issubdrg  19254  ply1scln0  20146  qsssubdrg  20290  alexsublem  22340  cphsubrglem  23468  cphreccllem  23469  mdegldg  24347  tglinethru  26108  footexALT  26190  footexlem2  26192  poimirlem26  34470  lkrpssN  35851  lnatexN  36467  lhpexle2lem  36697  lhpexle3lem  36699  cdlemg47  37424  cdlemk54  37646  tendoinvcl  37792  lcdlkreqN  38310  mapdh8ab  38465  jm2.26lem3  39104  ablsimpgfindlem1  40186  stoweidlem36  41885