Theorem neeqtrd 3003

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

Syntax hints:   → wi 4   = wceq 1547   ≠ wne 2934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ne 2935

This theorem is referenced by:  neeqtrrd  3008  3netr3d  3010  xaddass2  13194  xov1plusxeqvd  13443  smndex2dnrinv  18878  ablsimpgfindlem1  20076  issubdrg  20753  qsssubdrg  21402  ply1scln0  22278  alexsublem  24028  cphsubrglem  25163  cphreccllem  25164  mdegldg  26050  nosep2o  27665  noetainflem4  27723  tglinethru  28723  footexALT  28805  footexlem2  28807  nrt2irr  30562  sdrgdvcl  33384  sdrginvcl  33385  0ringprmidl  33533  0ringmon1p  33649  irngnzply1lem  33883  irngnminplynz  33905  minplym1p  33906  minplynzm1p  33907  algextdeglem4  33913  mh-inf3f1  36778  poimirlem26  38022  lkrpssN  39664  lnatexN  40280  lhpexle2lem  40510  lhpexle3lem  40512  cdlemg47  41237  cdlemk54  41459  tendoinvcl  41605  lcdlkreqN  42123  mapdh8ab  42278  aks6d1c5lem2  42632  aks6d1c7  42678  jm2.26lem3  43455  stoweidlem36  46487  addmodne  47821  p1modne  47824  m1modne  47825  minusmod5ne  47826  gpg5nbgrvtx03starlem2  48568  gpg5nbgrvtx13starlem2  48571  gpg5edgnedg  48629