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

Theorem neeqtrd 3020
 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 3011 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 235 1 (𝜑𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ≠ wne 2951 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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750  df-ne 2952 This theorem is referenced by:  neeqtrrd  3025  3netr3d  3027  xaddass2  12697  xov1plusxeqvd  12943  smndex2dnrinv  18159  ablsimpgfindlem1  19310  issubdrg  19641  qsssubdrg  20238  ply1scln0  21028  alexsublem  22757  cphsubrglem  23891  cphreccllem  23892  mdegldg  24779  tglinethru  26542  footexALT  26624  footexlem2  26626  0ringprmidl  31158  nosep2o  33482  noetainflem4  33540  poimirlem26  35397  lkrpssN  36773  lnatexN  37389  lhpexle2lem  37619  lhpexle3lem  37621  cdlemg47  38346  cdlemk54  38568  tendoinvcl  38714  lcdlkreqN  39232  mapdh8ab  39387  jm2.26lem3  40350  stoweidlem36  43079
 Copyright terms: Public domain W3C validator