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

Theorem neeqtrri 3087
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
Hypotheses
Ref Expression
neeqtrr.1 𝐴𝐵
neeqtrr.2 𝐶 = 𝐵
Assertion
Ref Expression
neeqtrri 𝐴𝐶

Proof of Theorem neeqtrri
StepHypRef Expression
1 neeqtrr.1 . 2 𝐴𝐵
2 neeqtrr.2 . . 3 𝐶 = 𝐵
32eqcomi 2833 . 2 𝐵 = 𝐶
41, 3neeqtri 3086 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wne 3014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-ne 3015
This theorem is referenced by:  1one2o  8265  cflim2  9683  pnfnemnf  10694  resslem  16557  basendxnplusgndx  16608  plusgndxnmulrndx  16617  basendxnmulrndx  16618  slotsbhcdif  16693  symgvalstruct  18525  rmodislmod  19702  cnfldfun  20159  xrsnsgrp  20183  zlmlem  20266  matvsca  21028  tnglem  23252  setsvtx  26834  resvlem  30940  limsucncmpi  33853  sn-1ne2  39400  mnringbased  40847  mnringaddgd  40852  mnringscad  40856  mnringvscad  40857
  Copyright terms: Public domain W3C validator