Theorem neeqtrd 2994

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  neeqtrrd  2999  3netr3d  3001  xaddass2  13210  xov1plusxeqvd  13459  smndex2dnrinv  18842  ablsimpgfindlem1  20039  issubdrg  20689  qsssubdrg  21343  ply1scln0  22178  alexsublem  23931  cphsubrglem  25077  cphreccllem  25078  mdegldg  25971  nosep2o  27594  noetainflem4  27652  tglinethru  28563  footexALT  28645  footexlem2  28647  nrt2irr  30402  sdrgdvcl  33249  sdrginvcl  33250  0ringprmidl  33420  0ringmon1p  33526  irngnzply1lem  33685  irngnminplynz  33702  minplym1p  33703  minplynzm1p  33704  algextdeglem4  33710  poimirlem26  37640  lkrpssN  39156  lnatexN  39773  lhpexle2lem  40003  lhpexle3lem  40005  cdlemg47  40730  cdlemk54  40952  tendoinvcl  41098  lcdlkreqN  41616  mapdh8ab  41771  aks6d1c5lem2  42126  aks6d1c7  42172  jm2.26lem3  42990  stoweidlem36  46034  addmodne  47345  p1modne  47348  m1modne  47349  minusmod5ne  47350  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx13starlem2  48063