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

Theorem neeqtrd 3011
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 3002 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 231 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wne 2941
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 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2729  df-ne 2942
This theorem is referenced by:  neeqtrrd  3016  3netr3d  3018  xaddass2  13123  xov1plusxeqvd  13369  smndex2dnrinv  18685  ablsimpgfindlem1  19845  issubdrg  20200  qsssubdrg  20809  ply1scln0  21614  alexsublem  23347  cphsubrglem  24493  cphreccllem  24494  mdegldg  25383  nosep2o  26982  noetainflem4  27040  tglinethru  27407  footexALT  27489  footexlem2  27491  sdrgdvcl  31902  sdrginvcl  31903  0ringprmidl  32044  0ringmon1p  32086  irngnzply1lem  32184  poimirlem26  36042  lkrpssN  37563  lnatexN  38180  lhpexle2lem  38410  lhpexle3lem  38412  cdlemg47  39137  cdlemk54  39359  tendoinvcl  39505  lcdlkreqN  40023  mapdh8ab  40178  jm2.26lem3  41234  stoweidlem36  44178
  Copyright terms: Public domain W3C validator