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

Step	Hyp	Ref	Expression
1		neeqtrr.1	. 2
2		neeqtrr.2	. . 3
3	2	eqcomi 2470	. 2
4	1, 3	neeqtri 2755	1

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