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

Theorem neeqtrrd 2897
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 2657 . 2 (𝜑𝐵 = 𝐶)
41, 3neeqtrd 2892 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wne 2823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824
This theorem is referenced by:  3netr4d  2900  ttukeylem7  9375  modsumfzodifsn  12783  znnenlem  14984  expnprm  15653  symgextf1lem  17886  isabvd  18868  flimclslem  21835  chordthmlem  24604  atandmtan  24692  dchrptlem3  25036  opphllem6  25689  signstfveq0a  30781  subfacp1lem5  31292  noetalem3  31990  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  cdleme40n  36073  cdleme40w  36075  cdlemg33c  36313  cdlemg33e  36315  trlcocnvat  36329  cdlemh2  36421  cdlemh  36422  cdlemj3  36428  cdlemk24-3  36508  cdlemkfid1N  36526  erng1r  36600  dvalveclem  36631  tendoinvcl  36710  tendolinv  36711  tendorinv  36712  dihatlat  36940  mapdpglem18  37295  mapdpglem22  37299  baerlem5amN  37322  baerlem5bmN  37323  baerlem5abmN  37324  mapdindp1  37326  mapdindp4  37329  hdmap14lem4a  37480  imo72b2lem0  38782  imo72b2lem2  38784  imo72b2lem1  38788  imo72b2  38792  islindeps2  42597
  Copyright terms: Public domain W3C validator