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

Theorem neeqtrrd 3015
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 2739 . 2 (𝜑𝐵 = 𝐶)
41, 3neeqtrd 3010 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wne 2940
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 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2941
This theorem is referenced by:  3netr4d  3018  ttukeylem7  10456  modsumfzodifsn  13855  expnprm  16779  symgextf1lem  19207  isabvd  20293  flimclslem  23351  chordthmlem  26198  atandmtan  26286  dchrptlem3  26630  noetasuplem4  27100  opphllem6  27736  unidifsnne  31506  pmtrcnel  31989  pmtrcnel2  31990  cycpmrn  32041  fedgmul  32383  irngnzply1  32422  signstfveq0a  33245  subfacp1lem5  33835  ovoliunnfl  36166  voliunnfl  36168  volsupnfl  36169  cdleme40n  38977  cdleme40w  38979  cdlemg33c  39217  cdlemg33e  39219  trlcocnvat  39233  cdlemh2  39325  cdlemh  39326  cdlemj3  39332  cdlemk24-3  39412  cdlemkfid1N  39430  erng1r  39504  dvalveclem  39534  tendoinvcl  39613  tendolinv  39614  tendorinv  39615  dihatlat  39843  mapdpglem18  40198  mapdpglem22  40202  baerlem5amN  40225  baerlem5bmN  40226  baerlem5abmN  40227  mapdindp1  40229  mapdindp4  40232  hdmap14lem4a  40380  uvcn0  40773  prjspner1  41007  nlimsuc  41801  imo72b2lem0  42526  imo72b2lem2  42528  imo72b2  42533  islindeps2  46650
  Copyright terms: Public domain W3C validator