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

Theorem neeqtrrd 3087
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 2824 . 2 (𝜑𝐵 = 𝐶)
41, 3neeqtrd 3082 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wne 3013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-ne 3014
This theorem is referenced by:  3netr4d  3090  ttukeylem7  9925  modsumfzodifsn  13300  expnprm  16226  symgextf1lem  18477  isabvd  19520  flimclslem  22520  chordthmlem  25337  atandmtan  25425  dchrptlem3  25769  opphllem6  26465  unidifsnne  30223  pmtrcnel  30660  pmtrcnel2  30661  cycpmrn  30712  fedgmul  30926  signstfveq0a  31745  subfacp1lem5  32328  noetalem3  33116  ovoliunnfl  34815  voliunnfl  34817  volsupnfl  34818  cdleme40n  37484  cdleme40w  37486  cdlemg33c  37724  cdlemg33e  37726  trlcocnvat  37740  cdlemh2  37832  cdlemh  37833  cdlemj3  37839  cdlemk24-3  37919  cdlemkfid1N  37937  erng1r  38011  dvalveclem  38041  tendoinvcl  38120  tendolinv  38121  tendorinv  38122  dihatlat  38350  mapdpglem18  38705  mapdpglem22  38709  baerlem5amN  38732  baerlem5bmN  38733  baerlem5abmN  38734  mapdindp1  38736  mapdindp4  38739  hdmap14lem4a  38887  imo72b2lem0  40394  imo72b2lem2  40396  imo72b2  40403  islindeps2  44466
  Copyright terms: Public domain W3C validator