Theorem neeqtrd 2997

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2929

This theorem is referenced by:  neeqtrrd  3002  3netr3d  3004  xaddass2  13149  xov1plusxeqvd  13398  smndex2dnrinv  18823  ablsimpgfindlem1  20021  issubdrg  20695  qsssubdrg  21363  ply1scln0  22206  alexsublem  23959  cphsubrglem  25104  cphreccllem  25105  mdegldg  25998  nosep2o  27621  noetainflem4  27679  tglinethru  28614  footexALT  28696  footexlem2  28698  nrt2irr  30453  sdrgdvcl  33265  sdrginvcl  33266  0ringprmidl  33414  0ringmon1p  33520  irngnzply1lem  33703  irngnminplynz  33725  minplym1p  33726  minplynzm1p  33727  algextdeglem4  33733  poimirlem26  37696  lkrpssN  39272  lnatexN  39888  lhpexle2lem  40118  lhpexle3lem  40120  cdlemg47  40845  cdlemk54  41067  tendoinvcl  41213  lcdlkreqN  41731  mapdh8ab  41886  aks6d1c5lem2  42241  aks6d1c7  42287  jm2.26lem3  43104  stoweidlem36  46144  addmodne  47454  p1modne  47457  m1modne  47458  minusmod5ne  47459  gpg5nbgrvtx03starlem2  48179  gpg5nbgrvtx13starlem2  48182  gpg5edgnedg  48240