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

Theorem neeqtrrd 3090
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 2827 . 2 (𝜑𝐵 = 𝐶)
41, 3neeqtrd 3085 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wne 3016
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 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-ne 3017
This theorem is referenced by:  3netr4d  3093  ttukeylem7  9926  modsumfzodifsn  13302  expnprm  16228  symgextf1lem  18479  isabvd  19522  flimclslem  22522  chordthmlem  25337  atandmtan  25425  dchrptlem3  25770  opphllem6  26466  unidifsnne  30224  pmtrcnel  30661  pmtrcnel2  30662  cycpmrn  30713  fedgmul  30927  signstfveq0a  31746  subfacp1lem5  32329  noetalem3  33117  ovoliunnfl  34816  voliunnfl  34818  volsupnfl  34819  cdleme40n  37486  cdleme40w  37488  cdlemg33c  37726  cdlemg33e  37728  trlcocnvat  37742  cdlemh2  37834  cdlemh  37835  cdlemj3  37841  cdlemk24-3  37921  cdlemkfid1N  37939  erng1r  38013  dvalveclem  38043  tendoinvcl  38122  tendolinv  38123  tendorinv  38124  dihatlat  38352  mapdpglem18  38707  mapdpglem22  38711  baerlem5amN  38734  baerlem5bmN  38735  baerlem5abmN  38736  mapdindp1  38738  mapdindp4  38741  hdmap14lem4a  38889  imo72b2lem0  40396  imo72b2lem2  40398  imo72b2lem1  40402  imo72b2  40406  islindeps2  44436
  Copyright terms: Public domain W3C validator