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 2743 . 2 (𝜑𝐵 = 𝐶)
41, 3neeqtrd 3010 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941
This theorem is referenced by:  3netr4d  3018  ttukeylem7  10555  modsumfzodifsn  13985  expnprm  16940  symgextf1lem  19438  isabvd  20813  flimclslem  23992  chordthmlem  26875  atandmtan  26963  dchrptlem3  27310  noetasuplem4  27781  opphllem6  28760  nrt2irr  30492  unidifsnne  32554  pmtrcnel  33109  pmtrcnel2  33110  cycpmrn  33163  qsdrnglem2  33524  fedgmul  33682  irngnzply1  33741  irredminply  33757  signstfveq0a  34591  subfacp1lem5  35189  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  cdleme40n  40470  cdleme40w  40472  cdlemg33c  40710  cdlemg33e  40712  trlcocnvat  40726  cdlemh2  40818  cdlemh  40819  cdlemj3  40825  cdlemk24-3  40905  cdlemkfid1N  40923  erng1r  40997  dvalveclem  41027  tendoinvcl  41106  tendolinv  41107  tendorinv  41108  dihatlat  41336  mapdpglem18  41691  mapdpglem22  41695  baerlem5amN  41718  baerlem5bmN  41719  baerlem5abmN  41720  mapdindp1  41722  mapdindp4  41725  hdmap14lem4a  41873  uvcn0  42552  prjspner1  42636  nlimsuc  43454  imo72b2lem2  44180  imo72b2  44185  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx13starlem2  48028  islindeps2  48400  fucofvalne  49020
  Copyright terms: Public domain W3C validator