Theorem neeqtrd 3002

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  neeqtrrd  3007  3netr3d  3009  xaddass2  13177  xov1plusxeqvd  13426  smndex2dnrinv  18855  ablsimpgfindlem1  20053  issubdrg  20728  qsssubdrg  21396  ply1scln0  22249  alexsublem  24003  cphsubrglem  25148  cphreccllem  25149  mdegldg  26042  nosep2o  27665  noetainflem4  27723  tglinethru  28724  footexALT  28806  footexlem2  28808  nrt2irr  30564  sdrgdvcl  33397  sdrginvcl  33398  0ringprmidl  33546  0ringmon1p  33654  irngnzply1lem  33872  irngnminplynz  33894  minplym1p  33895  minplynzm1p  33896  algextdeglem4  33902  poimirlem26  37901  lkrpssN  39543  lnatexN  40159  lhpexle2lem  40389  lhpexle3lem  40391  cdlemg47  41116  cdlemk54  41338  tendoinvcl  41484  lcdlkreqN  42002  mapdh8ab  42157  aks6d1c5lem2  42512  aks6d1c7  42558  jm2.26lem3  43362  stoweidlem36  46398  addmodne  47708  p1modne  47711  m1modne  47712  minusmod5ne  47713  gpg5nbgrvtx03starlem2  48433  gpg5nbgrvtx13starlem2  48436  gpg5edgnedg  48494