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

Theorem neeqtrd 3085
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 3076 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 233 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wne 3016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-ne 3017
This theorem is referenced by:  neeqtrrd  3090  3netr3d  3092  xaddass2  12633  xov1plusxeqvd  12874  ablsimpgfindlem1  19160  issubdrg  19491  ply1scln0  20389  qsssubdrg  20534  alexsublem  22582  cphsubrglem  23710  cphreccllem  23711  mdegldg  24589  tglinethru  26350  footexALT  26432  footexlem2  26434  poimirlem26  34800  lkrpssN  36181  lnatexN  36797  lhpexle2lem  37027  lhpexle3lem  37029  cdlemg47  37754  cdlemk54  37976  tendoinvcl  38122  lcdlkreqN  38640  mapdh8ab  38795  jm2.26lem3  39478  stoweidlem36  42202  smndex2dnrinv  43985
  Copyright terms: Public domain W3C validator