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

Theorem neeqtrri 2756
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 2470 . 2
41, 3neeqtri 2755 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  =/=wne 2652
This theorem is referenced by:  cflim2  8664  pnfnemnf  11355  resslem  14690  xrsnsgrp  18454  zlmlem  18554  matbas  18915  matplusg  18916  matvsca  18918  tnglem  21154  resvlem  27821  limsucncmpi  29910  uhgrepe  32378  slotsbhcdif  32559  plusgndxnmulrndx  32759  basendxnmulrndx  32760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654
  Copyright terms: Public domain W3C validator