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

Theorem neeqtrri 2854
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 2618 . 2 𝐵 = 𝐶
41, 3neeqtri 2853 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = 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:  cflim2  8945  pnfnemnf  11786  resslem  15706  slotsbhcdif  15849  xrsnsgrp  19547  zlmlem  19629  matbas  19980  matplusg  19981  matvsca  19983  tnglem  22192  resvlem  28968  limsucncmpi  31420  uhgrstrrepe  40299  plusgndxnmulrndx  41738  basendxnmulrndx  41739
  Copyright terms: Public domain W3C validator