Theorem neeqtrd 3029

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2960

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ne 2961

This theorem is used by:  neeqtrrd  3034  3netr3d  3036  xaddass2  13296  xov1plusxeqvd  13545  smndex2dnrinv  19018  ablsimpgfindlem1  20227  issubdrg  20937  0ringprmidl  21531  qsssubdrg  21630  ply1scln0  22506  alexsublem  24256  cphsubrglem  25391  cphreccllem  25392  mdegldg  26278  nosep2o  27901  noetainflem4  27959  tglinethru  28964  footexALT  29053  footexlem2  29055  lnssplng  29129  nrt2irr  30899  sdrgdvcl  33688  sdrginvcl  33689  0ringmon1p  33915  irngnzply1lem  34148  irngnminplynz  34170  minplym1p  34171  minplynzm1p  34172  algextdeglem4  34178  mh-inf3f1  37113  poimirlem26  38358  lkrpssN  39999  lnatexN  40615  lhpexle2lem  40845  lhpexle3lem  40847  cdlemg47  41572  cdlemk54  41794  tendoinvcl  41940  lcdlkreqN  42458  mapdh8ab  42613  aks6d1c5lem2  42967  aks6d1c7  43013  jm2.26lem3  43805  stoweidlem36  46827  addmodne  48164  p1modne  48167  m1modne  48168  minusmod5ne  48169  gpg5nbgrvtx03starlem2  48911  gpg5nbgrvtx13starlem2  48914  gpg5edgnedg  48972