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

Theorem neeqtrri 2896
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 2660 . 2 𝐵 = 𝐶
41, 3neeqtri 2895 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wne 2823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824
This theorem is referenced by:  cflim2  9123  pnfnemnf  10132  resslem  15980  basendxnplusgndx  16036  plusgndxnmulrndx  16045  basendxnmulrndx  16046  slotsbhcdif  16127  rmodislmod  18979  cnfldfun  19806  xrsnsgrp  19830  zlmlem  19913  matbas  20267  matplusg  20268  matvsca  20270  tnglem  22491  setsvtx  25972  resvlem  29959  limsucncmpi  32569
  Copyright terms: Public domain W3C validator