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

Theorem neeqtrd 3014
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 3005 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 231 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wne 2944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-ne 2945
This theorem is referenced by:  neeqtrrd  3019  3netr3d  3021  xaddass2  13176  xov1plusxeqvd  13422  smndex2dnrinv  18732  ablsimpgfindlem1  19893  issubdrg  20263  qsssubdrg  20872  ply1scln0  21678  alexsublem  23411  cphsubrglem  24557  cphreccllem  24558  mdegldg  25447  nosep2o  27046  noetainflem4  27104  tglinethru  27620  footexALT  27702  footexlem2  27704  sdrgdvcl  32116  sdrginvcl  32117  0ringprmidl  32262  0ringmon1p  32304  irngnzply1lem  32404  poimirlem26  36133  lkrpssN  37654  lnatexN  38271  lhpexle2lem  38501  lhpexle3lem  38503  cdlemg47  39228  cdlemk54  39450  tendoinvcl  39596  lcdlkreqN  40114  mapdh8ab  40269  jm2.26lem3  41354  stoweidlem36  44351
  Copyright terms: Public domain W3C validator