Theorem neeqtrd 3024

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

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

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 2155  ax-ext 2732

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

This theorem is used by:  neeqtrrd  3029  3netr3d  3031  xaddass2  13305  xov1plusxeqvd  13554  smndex2dnrinv  19030  ablsimpgfindlem1  20239  issubdrg  20949  0ringprmidl  21543  qsssubdrg  21642  ply1scln0  22520  alexsublem  24273  cphsubrglem  25408  cphreccllem  25409  mdegldg  26294  nosep2o  27921  noetainflem4  27979  tglinethru  28986  footexALT  29075  footexlem2  29077  lnssplng  29152  nrt2irr  30956  sdrgdvcl  33743  sdrginvcl  33744  0ringmon1p  33970  irngnzply1lem  34203  irngnminplynz  34225  minplym1p  34226  minplynzm1p  34227  algextdeglem4  34233  poimirlem26  38398  lkrpssN  40039  lnatexN  40655  lhpexle2lem  40885  lhpexle3lem  40887  cdlemg47  41612  cdlemk54  41834  tendoinvcl  41980  lcdlkreqN  42498  mapdh8ab  42653  aks6d1c5lem2  43007  aks6d1c7  43053  jm2.26lem3  43845  stoweidlem36  46867  addmodne  48241  p1modne  48244  m1modne  48245  minusmod5ne  48246  gpg5nbgrvtx03starlem2  48988  gpg5nbgrvtx13starlem2  48991  gpg5edgnedg  49049