Theorem neeqtrd 3005

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

Syntax hints:   → wi 4   = wceq 1548   ≠ wne 2936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-ne 2937

This theorem is referenced by:  neeqtrrd  3010  3netr3d  3012  xaddass2  13197  xov1plusxeqvd  13446  smndex2dnrinv  18881  ablsimpgfindlem1  20078  issubdrg  20755  qsssubdrg  21404  ply1scln0  22280  alexsublem  24030  cphsubrglem  25165  cphreccllem  25166  mdegldg  26052  nosep2o  27666  noetainflem4  27724  tglinethru  28724  footexALT  28806  footexlem2  28808  nrt2irr  30563  sdrgdvcl  33385  sdrginvcl  33386  0ringprmidl  33534  0ringmon1p  33650  irngnzply1lem  33884  irngnminplynz  33906  minplym1p  33907  minplynzm1p  33908  algextdeglem4  33914  mh-inf3f1  36782  poimirlem26  38026  lkrpssN  39668  lnatexN  40284  lhpexle2lem  40514  lhpexle3lem  40516  cdlemg47  41241  cdlemk54  41463  tendoinvcl  41609  lcdlkreqN  42127  mapdh8ab  42282  aks6d1c5lem2  42636  aks6d1c7  42682  jm2.26lem3  43459  stoweidlem36  46491  addmodne  47825  p1modne  47828  m1modne  47829  minusmod5ne  47830  gpg5nbgrvtx03starlem2  48572  gpg5nbgrvtx13starlem2  48575  gpg5edgnedg  48633