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

Syntax hints:   → wi 4   = wceq 1562   ≠ wne 2959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-ne 2960

This theorem is referenced by:  neeqtrrd  3033  3netr3d  3035  xaddass2  13255  xov1plusxeqvd  13504  smndex2dnrinv  18954  ablsimpgfindlem1  20151  issubdrg  20831  qsssubdrg  21480  ply1scln0  22356  alexsublem  24106  cphsubrglem  25241  cphreccllem  25242  mdegldg  26128  nosep2o  27748  noetainflem4  27806  tglinethru  28807  footexALT  28893  footexlem2  28895  lnssplng  29001  nrt2irr  30677  sdrgdvcl  33488  sdrginvcl  33489  0ringprmidl  33638  0ringmon1p  33755  irngnzply1lem  33989  irngnminplynz  34011  minplym1p  34012  minplynzm1p  34013  algextdeglem4  34019  mh-inf3f1  36906  poimirlem26  38150  lkrpssN  39792  lnatexN  40408  lhpexle2lem  40638  lhpexle3lem  40640  cdlemg47  41365  cdlemk54  41587  tendoinvcl  41733  lcdlkreqN  42251  mapdh8ab  42406  aks6d1c5lem2  42760  aks6d1c7  42806  jm2.26lem3  43583  stoweidlem36  46615  addmodne  47949  p1modne  47952  m1modne  47953  minusmod5ne  47954  gpg5nbgrvtx03starlem2  48696  gpg5nbgrvtx13starlem2  48699  gpg5edgnedg  48757