MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neeqtrd Structured version   Visualization version   GIF version

Theorem neeqtrd 3010
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
StepHypRef Expression
1 neeqtrd.1 . 2 (𝜑𝐴𝐵)
2 neeqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
32neeq2d 3001 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 232 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wne 2940
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 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941
This theorem is referenced by:  neeqtrrd  3015  3netr3d  3017  xaddass2  13292  xov1plusxeqvd  13538  smndex2dnrinv  18928  ablsimpgfindlem1  20127  issubdrg  20781  qsssubdrg  21444  ply1scln0  22295  alexsublem  24052  cphsubrglem  25211  cphreccllem  25212  mdegldg  26105  nosep2o  27727  noetainflem4  27785  tglinethru  28644  footexALT  28726  footexlem2  28728  nrt2irr  30492  sdrgdvcl  33301  sdrginvcl  33302  0ringprmidl  33477  0ringmon1p  33583  irngnzply1lem  33740  irngnminplynz  33755  minplym1p  33756  algextdeglem4  33761  poimirlem26  37653  lkrpssN  39164  lnatexN  39781  lhpexle2lem  40011  lhpexle3lem  40013  cdlemg47  40738  cdlemk54  40960  tendoinvcl  41106  lcdlkreqN  41624  mapdh8ab  41779  aks6d1c5lem2  42139  aks6d1c7  42185  jm2.26lem3  43013  stoweidlem36  46051  addmodne  47346  p1modne  47349  m1modne  47350  minusmod5ne  47351  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx13starlem2  48028
  Copyright terms: Public domain W3C validator