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

Theorem neeqtrrd 3085
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
Hypotheses
Ref Expression
neeqtrrd.1 (𝜑𝐴𝐵)
neeqtrrd.2 (𝜑𝐶 = 𝐵)
Assertion
Ref Expression
neeqtrrd (𝜑𝐴𝐶)

Proof of Theorem neeqtrrd
StepHypRef Expression
1 neeqtrrd.1 . 2 (𝜑𝐴𝐵)
2 neeqtrrd.2 . . 3 (𝜑𝐶 = 𝐵)
32eqcomd 2828 . 2 (𝜑𝐵 = 𝐶)
41, 3neeqtrd 3080 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wne 3011
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 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2815  df-ne 3012
This theorem is referenced by:  3netr4d  3088  ttukeylem7  9926  modsumfzodifsn  13307  expnprm  16227  symgextf1lem  18539  isabvd  19582  flimclslem  22587  chordthmlem  25416  atandmtan  25504  dchrptlem3  25848  opphllem6  26544  unidifsnne  30303  pmtrcnel  30764  pmtrcnel2  30765  cycpmrn  30816  fedgmul  31084  signstfveq0a  31920  subfacp1lem5  32505  noetalem3  33293  ovoliunnfl  35057  voliunnfl  35059  volsupnfl  35060  cdleme40n  37722  cdleme40w  37724  cdlemg33c  37962  cdlemg33e  37964  trlcocnvat  37978  cdlemh2  38070  cdlemh  38071  cdlemj3  38077  cdlemk24-3  38157  cdlemkfid1N  38175  erng1r  38249  dvalveclem  38279  tendoinvcl  38358  tendolinv  38359  tendorinv  38360  dihatlat  38588  mapdpglem18  38943  mapdpglem22  38947  baerlem5amN  38970  baerlem5bmN  38971  baerlem5abmN  38972  mapdindp1  38974  mapdindp4  38977  hdmap14lem4a  39125  imo72b2lem0  40802  imo72b2lem2  40804  imo72b2  40811  islindeps2  44831
  Copyright terms: Public domain W3C validator