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

Theorem neeqtrrd 2856
 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 2616 . 2 (𝜑𝐵 = 𝐶)
41, 3neeqtrd 2851 1 (𝜑𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1475   ≠ wne 2780 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782 This theorem is referenced by:  3netr4d  2859  ttukeylem7  9220  modsumfzodifsn  12605  znnenlem  14779  expnprm  15444  symgextf1lem  17663  isabvd  18643  flimclslem  21598  chordthmlem  24359  atandmtan  24447  dchrptlem3  24791  opphllem6  25444  isusgra0  25876  usgraop  25879  signstfveq0a  29979  subfacp1lem5  30420  nodenselem3  31082  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  cdleme40n  34774  cdleme40w  34776  cdlemg33c  35014  cdlemg33e  35016  trlcocnvat  35030  cdlemh2  35122  cdlemh  35123  cdlemj3  35129  cdlemk24-3  35209  cdlemkfid1N  35227  erng1r  35301  dvalveclem  35332  tendoinvcl  35411  tendolinv  35412  tendorinv  35413  dihatlat  35641  mapdpglem18  35996  mapdpglem22  36000  baerlem5amN  36023  baerlem5bmN  36024  baerlem5abmN  36025  mapdindp1  36027  mapdindp4  36030  hdmap14lem4a  36181  imo72b2lem0  37487  imo72b2lem2  37489  imo72b2lem1  37493  imo72b2  37497  islindeps2  42066
 Copyright terms: Public domain W3C validator