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

Theorem neeqtrri 3014
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 2746 . 2 𝐵 = 𝐶
41, 3neeqtri 3013 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941
This theorem is referenced by:  nlim1  8527  nlim2  8528  1one2o  8684  cflim2  10303  pnfnemnf  11316  resslemOLD  17288  basendxnmulrndx  17339  basendxnmulrndxOLD  17340  plusgndxnmulrndx  17341  slotsbhcdif  17459  slotsbhcdifOLD  17460  symgvalstructOLD  19415  cnfldfunALTOLDOLD  21393  xrsnsgrp  21420  zlmlemOLD  21528  matvscaOLD  22422  tnglemOLD  24654  slotsinbpsd  28449  slotslnbpsd  28450  setsvtx  29052  resvlemOLD  33358  limsucncmpi  36446  sn-1ne2  42300  mnringbasedOLD  44231  mnringaddgdOLD  44237  mnringscadOLD  44242  mnringvscadOLD  44244
  Copyright terms: Public domain W3C validator