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

Theorem neeqtrd 3009
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 3000 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 231 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wne 2939
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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-ne 2940
This theorem is referenced by:  neeqtrrd  3014  3netr3d  3016  xaddass2  13179  xov1plusxeqvd  13425  smndex2dnrinv  18739  ablsimpgfindlem1  19900  issubdrg  20296  qsssubdrg  20893  ply1scln0  21699  alexsublem  23432  cphsubrglem  24578  cphreccllem  24579  mdegldg  25468  nosep2o  27067  noetainflem4  27125  tglinethru  27641  footexALT  27723  footexlem2  27725  sdrgdvcl  32145  sdrginvcl  32146  0ringprmidl  32298  0ringmon1p  32340  irngnzply1lem  32451  poimirlem26  36177  lkrpssN  37698  lnatexN  38315  lhpexle2lem  38545  lhpexle3lem  38547  cdlemg47  39272  cdlemk54  39494  tendoinvcl  39640  lcdlkreqN  40158  mapdh8ab  40313  jm2.26lem3  41383  stoweidlem36  44397
  Copyright terms: Public domain W3C validator