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

Theorem neeqtrri 2855
 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 2619 . 2 𝐵 = 𝐶
41, 3neeqtri 2854 1 𝐴𝐶
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475   ≠ wne 2780 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782 This theorem is referenced by:  cflim2  8968  pnfnemnf  9973  resslem  15760  slotsbhcdif  15903  xrsnsgrp  19601  zlmlem  19684  matbas  20038  matplusg  20039  matvsca  20041  tnglem  22254  uhgrstrrepe  25745  resvlem  29162  limsucncmpi  31614  plusgndxnmulrndx  41743  basendxnmulrndx  41744
 Copyright terms: Public domain W3C validator