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

Theorem neeqtrd 3000
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 2991 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 231 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1534  wne 2930
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-ne 2931
This theorem is referenced by:  neeqtrrd  3005  3netr3d  3007  xaddass2  13283  xov1plusxeqvd  13529  smndex2dnrinv  18905  ablsimpgfindlem1  20107  issubdrg  20759  qsssubdrg  21423  ply1scln0  22283  alexsublem  24039  cphsubrglem  25196  cphreccllem  25197  mdegldg  26093  nosep2o  27712  noetainflem4  27770  tglinethru  28563  footexALT  28645  footexlem2  28647  nrt2irr  30406  sdrgdvcl  33149  sdrginvcl  33150  0ringprmidl  33324  0ringmon1p  33430  irngnzply1lem  33566  irngnminplynz  33581  minplym1p  33582  algextdeglem4  33587  poimirlem26  37347  lkrpssN  38861  lnatexN  39478  lhpexle2lem  39708  lhpexle3lem  39710  cdlemg47  40435  cdlemk54  40657  tendoinvcl  40803  lcdlkreqN  41321  mapdh8ab  41476  aks6d1c5lem2  41836  aks6d1c7  41882  jm2.26lem3  42659  stoweidlem36  45657
  Copyright terms: Public domain W3C validator