Theorem neeqtrd 2995

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

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

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 2702

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

This theorem is referenced by:  neeqtrrd  3000  3netr3d  3002  xaddass2  13217  xov1plusxeqvd  13466  smndex2dnrinv  18849  ablsimpgfindlem1  20046  issubdrg  20696  qsssubdrg  21350  ply1scln0  22185  alexsublem  23938  cphsubrglem  25084  cphreccllem  25085  mdegldg  25978  nosep2o  27601  noetainflem4  27659  tglinethru  28570  footexALT  28652  footexlem2  28654  nrt2irr  30409  sdrgdvcl  33256  sdrginvcl  33257  0ringprmidl  33427  0ringmon1p  33533  irngnzply1lem  33692  irngnminplynz  33709  minplym1p  33710  minplynzm1p  33711  algextdeglem4  33717  poimirlem26  37647  lkrpssN  39163  lnatexN  39780  lhpexle2lem  40010  lhpexle3lem  40012  cdlemg47  40737  cdlemk54  40959  tendoinvcl  41105  lcdlkreqN  41623  mapdh8ab  41778  aks6d1c5lem2  42133  aks6d1c7  42179  jm2.26lem3  42997  stoweidlem36  46041  addmodne  47349  p1modne  47352  m1modne  47353  minusmod5ne  47354  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx13starlem2  48067