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

Theorem neeqtrd 3055
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 3046 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 233 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1525  wne 2986
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-9 2093  ax-ext 2771
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-cleq 2790  df-ne 2987
This theorem is referenced by:  neeqtrrd  3060  3netr3d  3062  xaddass2  12497  xov1plusxeqvd  12738  issubdrg  19254  ply1scln0  20146  qsssubdrg  20290  alexsublem  22340  cphsubrglem  23468  cphreccllem  23469  mdegldg  24347  tglinethru  26108  footexALT  26190  footexlem2  26192  poimirlem26  34470  lkrpssN  35851  lnatexN  36467  lhpexle2lem  36697  lhpexle3lem  36699  cdlemg47  37424  cdlemk54  37646  tendoinvcl  37792  lcdlkreqN  38310  mapdh8ab  38465  jm2.26lem3  39104  ablsimpgfindlem1  40186  stoweidlem36  41885
  Copyright terms: Public domain W3C validator