Theorem neeqtrd 3028

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-ne 2960

This theorem is used by:  neeqtrrd  3033  3netr3d  3035  xaddass2  13393  xov1plusxeqvd  13642  smndex2dnrinv  19129  ablsimpgfindlem1  20338  issubdrg  21052  0ringprmidl  21648  qsssubdrg  21747  ply1scln0  22625  alexsublem  24378  cphsubrglem  25513  cphreccllem  25514  mdegldg  26399  nosep2o  28054  noetainflem4  28112  tglinethru  29119  footexALT  29208  footexlem2  29210  lnssplng  29285  nrt2irr  31089  sdrgdvcl  33917  sdrginvcl  33918  0ringmon1p  34145  irngnzply1lem  34378  irngnminplynz  34400  minplym1p  34401  minplynzm1p  34402  algextdeglem4  34408  poimirlem26  38710  lkrpssN  40366  lnatexN  40982  lhpexle2lem  41212  lhpexle3lem  41214  cdlemg47  41939  cdlemk54  42161  tendoinvcl  42307  lcdlkreqN  42825  mapdh8ab  42980  aks6d1c5lem2  43334  aks6d1c7  43380  frlmnzcoordsca  43804  prjspnnorm  43807  jm2.26lem3  44154  stoweidlem36  47191  addmodne  48565  p1modne  48568  m1modne  48569  minusmod5ne  48570  gpg5nbgrvtx03starlem2  49312  gpg5nbgrvtx13starlem2  49315  gpg5edgnedg  49373