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

Theorem neeqtrrd 2855
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 2615 . 2 (𝜑𝐵 = 𝐶)
41, 3neeqtrd 2850 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wne 2779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602  df-ne 2781
This theorem is referenced by:  3netr4d  2858  ttukeylem7  9197  modsumfzodifsn  12560  znnenlem  14725  expnprm  15390  symgextf1lem  17609  isabvd  18589  flimclslem  21540  chordthmlem  24276  atandmtan  24364  dchrptlem3  24708  opphllem6  25362  isusgra0  25642  usgraop  25645  signstfveq0a  29785  subfacp1lem5  30226  nodenselem3  30888  ovoliunnfl  32417  voliunnfl  32419  volsupnfl  32420  cdleme40n  34570  cdleme40w  34572  cdlemg33c  34810  cdlemg33e  34812  trlcocnvat  34826  cdlemh2  34918  cdlemh  34919  cdlemj3  34925  cdlemk24-3  35005  cdlemkfid1N  35023  erng1r  35097  dvalveclem  35128  tendoinvcl  35207  tendolinv  35208  tendorinv  35209  dihatlat  35437  mapdpglem18  35792  mapdpglem22  35796  baerlem5amN  35819  baerlem5bmN  35820  baerlem5abmN  35821  mapdindp1  35823  mapdindp4  35826  hdmap14lem4a  35977  imo72b2lem0  37283  imo72b2lem2  37285  imo72b2lem1  37289  imo72b2  37293  islindeps2  42061
  Copyright terms: Public domain W3C validator