Theorem neeqtrd 3025

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

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

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 2733

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

This theorem is used by:  neeqtrrd  3030  3netr3d  3032  xaddass2  13380  xov1plusxeqvd  13629  smndex2dnrinv  19114  ablsimpgfindlem1  20323  issubdrg  21037  0ringprmidl  21633  qsssubdrg  21732  ply1scln0  22610  alexsublem  24363  cphsubrglem  25498  cphreccllem  25499  mdegldg  26384  nosep2o  28039  noetainflem4  28097  tglinethru  29104  footexALT  29193  footexlem2  29195  lnssplng  29270  nrt2irr  31074  sdrgdvcl  33861  sdrginvcl  33862  0ringmon1p  34089  irngnzply1lem  34322  irngnminplynz  34344  minplym1p  34345  minplynzm1p  34346  algextdeglem4  34352  poimirlem26  38564  lkrpssN  40220  lnatexN  40836  lhpexle2lem  41066  lhpexle3lem  41068  cdlemg47  41793  cdlemk54  42015  tendoinvcl  42161  lcdlkreqN  42679  mapdh8ab  42834  aks6d1c5lem2  43188  aks6d1c7  43234  frlmnzcoordsca  43658  prjspnnorm  43661  jm2.26lem3  44007  stoweidlem36  47045  addmodne  48419  p1modne  48422  m1modne  48423  minusmod5ne  48424  gpg5nbgrvtx03starlem2  49166  gpg5nbgrvtx13starlem2  49169  gpg5edgnedg  49227