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

Theorem neeqtrd 2845
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 2836 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 220 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wne 2774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-ext 2584
This theorem depends on definitions:  df-bi 195  df-cleq 2597  df-ne 2776
This theorem is referenced by:  neeqtrrd  2850  3netr3d  2852  xaddass2  11904  xov1plusxeqvd  12140  issubdrg  18569  ply1scln0  19423  qsssubdrg  19565  alexsublem  21595  cphsubrglem  22704  cphreccllem  22705  mdegldg  23542  tglinethru  25244  footex  25326  eupath2lem3  26267  poimirlem26  32403  lkrpssN  33266  lnatexN  33881  lhpexle2lem  34111  lhpexle3lem  34113  cdlemg47  34840  cdlemk54  35062  tendoinvcl  35209  lcdlkreqN  35727  mapdh8ab  35882  jm2.26lem3  36384  stoweidlem36  38728
  Copyright terms: Public domain W3C validator