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

Theorem neeqtrd 3012
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 3003 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 222 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wne 2943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-ne 2944
This theorem is referenced by:  neeqtrrd  3017  3netr3d  3019  xaddass2  12285  xov1plusxeqvd  12525  issubdrg  19015  ply1scln0  19876  qsssubdrg  20020  alexsublem  22068  cphsubrglem  23196  cphreccllem  23197  mdegldg  24046  tglinethru  25752  footex  25834  poimirlem26  33768  lkrpssN  34972  lnatexN  35587  lhpexle2lem  35817  lhpexle3lem  35819  cdlemg47  36545  cdlemk54  36767  tendoinvcl  36914  lcdlkreqN  37432  mapdh8ab  37587  jm2.26lem3  38094  stoweidlem36  40770
  Copyright terms: Public domain W3C validator